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

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