ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] type free logic and higher order quantification

 To: ontolog-forum@xxxxxxxxxxxxxxxx Christopher Menzel Fri, 19 Aug 2011 14:56:14 -0500 <1313783774.5073.7.camel@xxxxxxxxxxxxxxxxx>
 ```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) ```
 Current Thread [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, Pat Hayes Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, John F. Sowa Re: [ontolog-forum] type free logic and higher order quantification, Pat Hayes Re: [ontolog-forum] type free logic and higher order quantification, John F. Sowa Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel <= Re: [ontolog-forum] type free logic and higher order quantification, Pat Hayes Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, k Goodier Re: [ontolog-forum] type free logic and higher order quantification, Christopher Menzel Re: [ontolog-forum] type free logic and higher order quantification, Rick Murphy Re: [ontolog-forum] type free logic and higher order quantification, John F. Sowa