Re: circular paradox gizmo

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 .


peter

Received on Friday, 3 May 2002 11:12:31 UTC