On Fri, 2011-08-19 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
> first-order style of semantics) and the kind of higher-order 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 higher-order logic, should *not* be considered part of
> logic. They should be considered a version of set theory. (01)
Well, the issue of whether higher-order 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 First-order Logic" and "Beyond First-order Logic: The
Historical Interplay between Mathematical Logic and Axiomatic Set
Theory"; use The Google for citation details; also Matti Eklund, "On How
Logic Became First-order". There is Stewart Shapiro's excellent
"Foundations without Foundationalism," an extended defense of the thesis
that second-order 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 first-order,
> >> and would likely find CL congenial. If it seems obviously "yes",
> >> then you are thinking in a genuinely higher-order 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 higher-order
> 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 higher-order
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 second-order
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 "second-order" logic that has been given a
Henkin-style "general" model theory and hence is semantically
first-order (hence the scare quotes). Given (R a) and (Q b), (exists
(P) (and (P a) (P b))) follows from the second-order 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
so-called "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 self-predication 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 type-free, 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/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (024)
|