# 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

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 UTC

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