On Fri, 20110819 at 10:31 0400, John F. Sowa wrote:
> Rick,
>
> As Pat emphasized, there is a huge semantic difference between
> quantifying over relations (which can be done in Common Logic with a
> firstorder style of semantics) and the kind of higherorder logic
> that logicians have been kicking around.
>
> In fact, many logicians have now come to believe that the infinite
> hierarchy of relations, relations of relations, etc., which are
> assumed for higherorder logic, should *not* be considered part of
> logic. They should be considered a version of set theory. (01)
Well, the issue of whether higherorder logic really deserves the name
is a difficult one dating back at least to a squabble between Zermelo
(yea) and Skolem (nay) and the debate is in fact still lively and the
issue largely unsettled. (For the Zermelo/Skolem controversy, see the
two papers by the terrific historian of logic Gregory Moore, "The
Emergence of Firstorder Logic" and "Beyond Firstorder Logic: The
Historical Interplay between Mathematical Logic and Axiomatic Set
Theory"; use The Google for citation details; also Matti Eklund, "On How
Logic Became Firstorder". There is Stewart Shapiro's excellent
"Foundations without Foundationalism," an extended defense of the thesis
that secondorder logic is indeed logic.) (02)
> PH
> >> Ask yourself whether [axioms (R a) and (Q b)] entail the following:
> >>
> >> (exists (p)(and (p a)(p b) )
> >>
> >> i.e. that there is a property that applies both to a and to b.
> >>
> >> If you intuitively answer "no", then you are thinking firstorder,
> >> and would likely find CL congenial. If it seems obviously "yes",
> >> then you are thinking in a genuinely higherorder way.
> >>
> >> It really does matter which way you choose, as you will be
> >> interested in very different logics.
>
> RM
> > Understood. I've been heads down on functional programming lately, so
> > I'm getting more comfy with higher order thinking.
>
> But the usual versions of functional programming are not higherorder
> in the way logicians use the term.
>
> For Pat's example, the axioms (R a) and (Q b) can be satisfied in
> a CL domain that has only four entities: {R, Q, a, b}. (03)
Note I had assumed that Pat meant his premises to be (R a) and (R b),
not (R a) and (Q b). I therefore thought his "test" for higherorder
thinking was whether one thought one could existentially generalize on
predicates, but perhaps I was hasty and misunderstood him. (In fact, I
think I must have, as he knows full well that the ability to
existentially generalize on predicates doesn't require full secondorder
logic.) (04)
> In that model, there is no p such that (p a) and (p b) are both true.
> Therefore the statement (exists (p) (and (p a)(p b)) is false.
>
> But in the logicians' version of higher order logic, for any domain
> of individuals such as {a,b}, there is an infinite hierarchy of
> domains of all possible relations over the domain {a,b}, relations
> of relations over that domain, ...
>
> Since all possible relations are included, there would have to be
> some relation p such that (p a) and (p b). (05)
Yes, but it also follows in "secondorder" logic that has been given a
Henkinstyle "general" model theory and hence is semantically
firstorder (hence the scare quotes). Given (R a) and (Q b), (exists
(P) (and (P a) (P b))) follows from the secondorder comprehension
principle (06)
(exists (P) (forall (x) (iff (P x) (or (R x) (Q x))))). (07)
It does *not* follow in CL because CL does not include any comprehension
principles. (08)
> RM
> > to establish a hierarchy of types to avoid paradox.
>
> You don't need a hierarchy of types to avoid paradox. (09)
Very true. (010)
> In CL, the statement equivalent to Russell's paradox (011)
I'd say: The sentence that *generates* Russell's paradox... (012)
> has a stable truth value: false. No paradox. (013)
Right. In more detail: the chief culprit in Russell's paradox is the
socalled "naive" comprehension principle that, for any formula φ there
is a set containing (or a property true of) all the things that are φ.
In the CL dialect CLIF, this principle is expressed schematically as: (014)
NC (exists (p) (forall (q) (iff (p x) φ))). (015)
In CL, where selfpredication is permitted, an instance of NC is: (016)
R (exists (p) (forall (q) (iff (p x) (not q q)))). (017)
A contradiction follows from R immediately. For let r be one of the
things p said to exist by R: (018)
(1) (forall (q) (iff (r x) (not q q)))). (019)
But CL is typefree, so r itself is among the things being quantified
over; so by universal instantiation: (020)
(2) (iff (r r) (not r r)), (021)
contradiction. So, as John notes, in CL, sentence R is false; more
exactly, it is *logically* false; its negation is a theorem of CL. (022)
chris (023)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgibin/wiki.pl?WikiHomePage#nid1J (024)
