From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>

Date: Fri, 03 May 2002 11:12:21 -0400

To: jos.deroo.jd@belgium.agfa.com

Cc: www-webont-wg@w3.org

Message-Id: <20020503111221Q.pfps@research.bell-labs.com>

Date: Fri, 03 May 2002 11:12:21 -0400

To: jos.deroo.jd@belgium.agfa.com

Cc: www-webont-wg@w3.org

Message-Id: <20020503111221Q.pfps@research.bell-labs.com>

From: "Jos De_Roo" <jos.deroo.jd@belgium.agfa.com> Subject: Re: circular paradox gizmo Date: Fri, 3 May 2002 14:32:05 +0200 [...] > >> I would make the claim that one cannot prove nor > >> disprove a paradox, we just have incompleteness > >> (no evidence/correspondence) > > > >Generally, paradoxes are paradoxes because you can (or should be able to) > >both prove and disprove them (at least in one way of thinking about > >paradoxes). > > I'm just curious to see a SOUND PROOF ARGUMENT for your latest paradox > I mean an ARGUMENT as a pair of things: > a set of sentences, the PREMISES; > a sentence, the CONCLUSION. > An argument is VALID if and only if it is necessary that > if all its premises are true, its conclusion is true. > An argument is SOUND if and only if it is valid and all > its premises are true. > A sound argument can be the premis of another sound argument. > > so > { true-statements } log:implies { conclusion-statement } . > is actually > conclusion-statement . > > If we can't soundly prove a paradox, then we should maybe live with them I just sent out a message showing that Jeremy's comprehension axioms lead to a contradiction. A similar proof can be done for my most recent paradox, but you need some background. It goes something like this: Comprehension axioms: CJ: all of Jeremy's comprehension axioms CC: a comprehension axiom like the axiom for subst in KIF - i.e., turn a non-circular class into a circular class - this comprehension axiom is rather hard to do correctly here Standard axioms: Axioms that determine the extension of classes, as in the axiomatization for DAML+OIL, in particular Deduction: You also need some deduction mechanism. I'll use something like natural deduction. To get around the lack of negation, I'll have to use complement directly to get contradictions. (Yes, this is rather informal.) The derivation the goes something like: CJ: produce _:1 owl:onProperty rdf:type . _:1 owl:hasClass _:2 . _:2 owl:OneOf _:3 . _:3 owl:first _:4 . _:3 owl:rest owl:nil . _:4 owl:complementOf _:5 . CC: produce _:6 owl:onProperty rdf:type . _:6 owl:hasClass _:7 . _:7 owl:OneOf _:8 . _:8 owl:first _:9 . _:9 owl:rest owl:nil . _:9 owl:complementOf _:6 . ND: Assume rdfs:Class rdf:type _:6 . Axioms for hasClass rdfs:Class rdf:type _:10 . _:10 rdf:type _:7 . Axioms for OneOf rdfs:Class rdf:type _:9 . This produces a contradiction so we derive rdfs:Class rdf:type _:11 . _:11 owl:complementOf _:6 Axioms for complementOf rdfs:Class rdf:type _:9 . Axioms for hasClass rdfs:Class rdf:type _:6 . But _:9 owl:complementOf _:6 . peterReceived on Friday, 3 May 2002 11:12:31 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:56:43 UTC
*