[Top] [All Lists]

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

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Thu, 18 Aug 2011 17:52:49 -0500
Message-id: <66116D87-6E0D-4D06-8FD0-CC7D6275925C@xxxxxxxx>
On Aug 18, 2011, at 5:15 PM, Pat Hayes wrote:
> ...
> Here is a test case to hone your intuitions. Consider these axioms:
> (R a)
> (Q b)    (01)

Pat, you obviously meant to write:    (02)

(R a)
(R b)    (03)

> 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.    (04)

I agree that's a good place to start for testing your intuitions, but answering 
"yes" here does not necessarily mean that you are thinking in a genuinely 
higher-order way, i.e., in a way that commits you to full second-order logic. 
For we can in fact add all of the comprehension axioms    (05)

  (exists (p) (forall (x1 ... xn) (iff (p x1 ... xn) φ)))    (06)

to the usual axioms for second-order quantification and the resulting logic can 
still be given a Henkin-style general model theory that renders the logic 
semantically first-order.  The comprehension axiom with φ = "(R x)" and some 
simple logic give us the implication in your example.    (07)

This, of course, only strengthens your initial point to Rick that "you need to 
be achingly precise about what you count as 'higher order'".    (08)

-chris    (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>