ontolog-forum
[Top] [All Lists]

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

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Rick Murphy <rick@xxxxxxxxxxxxxx>
Date: Fri, 19 Aug 2011 09:12:43 -0400
Message-id: <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)

<Prev in Thread] Current Thread [Next in Thread>