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

From: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>
Date: Tue, 21 May 2002 16:14:15 +0200

Cc: "www-webont-wg" <www-webont-wg@w3.org>
Message-ID: <OF50B6D852.9A5C684D-ONC1256BC0.004BBE7B@agfa.be>
```
> This example uses a natural deduction-style proof system.
>
>
> Axioms about the Russell set:
>     a/  ?x a :R   ->   ?x a [ owl:complementOf ?x ]
>     b/  ?x a [ owl:complementOf ?x ]   ->  ?x a :R
>
>     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

see & agree
as said last night, we have it that the consequent
of an asserted implication can't be not() or not(s)
so our stuff is incomplete (but consistent I hope)

--
Jos
```
Received on Tuesday, 21 May 2002 11:04:48 UTC

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