ontolog-forum
[Top] [All Lists]

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

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: k Goodier <kgoodier@xxxxxxxxxxx>
Date: Fri, 19 Aug 2011 19:27:37 -0400
Message-id: <1DC9F8BA-624F-42D0-94ED-3038A5C74D1F@xxxxxxxxxxx>
Why do we still use analogies like "long in the tooth" which harken back to our 
horse trading days?    (01)

Sent from my iPhone    (02)

On Aug 19, 2011, at 6:53 PM, Rick Murphy <rick@xxxxxxxxxxxxxx> wrote:    (03)

> Chris, thank you. The explanation below is very helpful in answering my
> question regarding predicativity in logics with FO semantics and HO
> syntax.
> 
> I enjoyed your paper [1] and recommend it highly for anyone who wants to
> understand the design goals of CL.
> 
> --
> Rick
> 
> [1] http://cmenzel.org/Papers/Menzel-KRTheWWWAndTheEvolutionOfLogic.pdf
> 
> On Fri, 2011-08-19 at 14:56 -0500, Christopher Menzel wrote:
> 
>>> In CL, the statement equivalent to Russell's paradox 
>> 
>> I'd say: The sentence that *generates* Russell's paradox...
>> 
>>> has a stable truth value: false.  No paradox.
>> 
>> 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:
>> 
>>  NC  (exists (p) (forall (q) (iff (p x) φ))).
>> 
>> In CL, where self-predication is permitted, an instance of NC is:
>> 
>>  R   (exists (p) (forall (q) (iff (p x) (not q q)))).
>> 
>> A contradiction follows from R immediately. For let r be one of the
>> things p said to exist by R:
>> 
>>  (1)  (forall (q) (iff (r x) (not q q)))).
>> 
>> But CL is type-free, so r itself is among the things being quantified
>> over; so by universal instantiation:
>> 
>>  (2)  (iff (r r) (not r r)),
>> 
>> contradiction.  So, as John notes, in CL, sentence R is false; more
>> exactly, it is *logically* false; its negation is a theorem of CL.
>> 
>> -chris
>> 
>> 
>> 
>> 
>> 
>> 
>> 
>> _________________________________________________________________
>> 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
>> 
> 
> 
> 
> _________________________________________________________________
> 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    (04)

_________________________________________________________________
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    (05)

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