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)
|