ontolog-forum
[Top] [All Lists]

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

 To: "[ontolog-forum]" Rick Murphy Fri, 19 Aug 2011 09:12:43 -0400 <1313759563.30871.607.camel@metho-laptop>
 ```Many thanks, Pat. See below.    (01) On Thu, 2011-08-18 at 17:15 -0500, Pat Hayes wrote: > On Aug 18, 2011, at 4:58 PM, Rick Murphy wrote: > > > Hey All: > > > > Long time no ont. > > > > I am researching type free logics with higher order quantification. > > You need to be achingly precise about what you count as 'higher order'. >Common Logic is type-free and (some would say) uses (what certainly looks very >like) higher-order quantification, in that it allows one to quantify over >names in predicate and function positions, like this: > > (forall (f)(iff (transitive f)(forall x y z)(if (and (f x y)(f y z)) (f x z) >)) ))    (02) I see. For example the term higher order quantification of 3.4.4 in Chris' paper would differ from universal quantification over types in the Girard-Reynolds polymorphic (second order) lambda calculus.    (03) > However, CL has a first-order semantics and its metatheory is much closer to >FO than HO, so many logicians would *not* count it as a higher-order logic. It >has been called FO logic with a HO syntax, or HO logic with a FO semantics.    (04) Got it. I found papers on HiLog and F-Logic.    (05) Is predicativity a relevant theme in the literature on FO semantics and HO syntax? The use of the term predicativity in the sense of the literature on intuitionistic logic is to establish a hierarchy of types to avoid paradox.    (06) > Here is a test case to hone your intuitions. Consider these axioms: > > (R a) > (Q b) > > And ask yourself whether these 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.    (07) Understood. I've been heads down on functional programming lately, so I'm getting more comfy with higher order thinking.    (08) > Pat > > > > > I > > would like to read some (free) academic research on this topic and > > wondered whether anyone could point me at published papers. > > > > Google only matches six documents on the terms "type free logic" and > > "higher order quantification". > > > > Research here seems thin, probably my ignorance. > > > > Chris I have read your paper. The references don't seem to point at > > direct prior research on these combined subjects. > > > > -- > > Rick > > > > > > _________________________________________________________________ > > 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 > > > > > > ------------------------------------------------------------ > IHMC (850)434 8903 or (650)494 3973 > 40 South Alcaniz St. (850)202 4416 office > Pensacola (850)202 4440 fax > FL 32502 (850)291 0667 mobile > phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes > > > > > >    (09) _________________________________________________________________ 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    (010) ```
 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 <=