W3C home > Mailing lists > Public > www-webont-wg@w3.org > May 2002

A derivation of a contradiction from the Russell set (was Re: ISSUE: DAML+OIL semantics is too weak)

From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
Date: Mon, 20 May 2002 15:31:51 -0400
To: jos.deroo.jd@belgium.agfa.com
Cc: www-webont-wg@w3.org
Message-Id: <20020520153151K.pfps@research.bell-labs.com>

This example uses a natural deduction-style proof system.  

Additional axioms

Axioms about the Russell set:
    a/  ?x a :R   ->   ?x a [ owl:complementOf ?x ]
    b/  ?x a [ owl:complementOf ?x ]   ->  ?x a :R

Axioms about complementOf:
    c/  ?x a [ owl:complementOf ?y ]   ->  not ( ?x a ?y )
    d/  not ( ?x a ?y ) ->  ?x a [ owl:complementOf ?y ]


Proof:

| :R a :R					Assumption
|--------
| :R a :R  ->  :R a [ owl:complementOf :R ]	a/ (universal elimination)
|
| :R a [owl:complementOf ?x]			-> elimination
|
| :R a [owl:complementOf :R] -> not(:R a :R )	c/ (universal elimination)
|
| not(:R a :R)					-> elimination
|
| FALSE						not elimination

not(:R a :R)					not introduction

| not(:R a :R)					Assumption
|-------------
| not ( :R a :R ) -> :R a [owl:complementOf :R]	d/ (universal elimination)
|
| :R a [ owl:complementOf :R ]			-> elimination
|
| :R a [ owl:complementOf :R ]   ->  :R a :R	b/ (universal elimination)
|
| :R a :R					-> elimination
|
| FALSE						not elimination

not(not(:R a :R))				not introduction

FALSE						not elimination
Received on Monday, 20 May 2002 15:33:16 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:50 GMT