Undecidability of OWL-Full and Cantor's antinomy

Hi!

I recently read the discussion about undecidability of OWL-Full, which
took place here several weeks ago in thread

    "Readings on OWL's (un)decidability?"

    From: Yoshio Fukushige <fukushige.yoshio@jp.panasonic.com>
    Date: Mon, 02 Oct 2006 15:28:15 +0900
    URL: http://lists.w3.org/Archives/Public/semantic-web/2006Oct/0005.html

Well, I have never before dealt with this issue, so after reading the
thread, I tried to make up some good example which might help me to
better understand this "undecidability problem" in OWL-Full. I finally
came up with the idea to define within OWL-Full Cantor's well known set
of all those sets, which do not have them self as an instance:

    (1) C := { m | m NOTIN m }

where "NOTIN" means "is not an instance of". This definition is
equivalent to

    (2) C := { m | m IN \m }

where "\m" denotes the complement of m. The problem with this set
becomes obvious when one asks, if C is an instance of itself, or not:

    (3) C IN C <==> C IN { m | m IN \m } <==> C IN \C <==> C NOTIN C

So from the definition of set C one can conclude a contradiction. And
this means that, if one defines this set within some OWL ontology, there
is some query of the form "Is x in M?" (with x = M := C), which cannot
be answered by any algorithm. Thus, OWL-Full would be undecidable.

First, it is clear that one can *not* create such a definition within
the DL dialect of OWL: The variable m from the expression "m IN \m" must
be an owl:Class, because only for a class m it is allowed to build its
complement "\m". So, one would have to create a statement like (in N3
notation):

    (4) :m rdf:type [ owl:complementOf :m ] .

where both :m and "[ owl:complementOf :m ]" are classes, and this is not
allowed in OWL-DL.

But this would not be a show stopper within OWL-Full, where a class
*can* be an instance of another class. So the question remains,
how to define the class C in OWL-Full in an analog way to eq.(2) above?
Looking at eq.(4), I was thinking about defining some owl:Restriction on
property 'rdf:type', so C would become something like:

    (5) :C a owl:Class ;
          owl:equivalentClass [ a owl:Restriction ;
            owl:onProperty rdf:type ;
            owl:allValuesFrom [ owl:complementOf :m ]  # WRONG!
          ] .

Of course, this does not work, because this expression has another
meaning than the expression in eq.(2): Eq.(5) would mean:

    C is the class of all those things x,
    which are instances of the complement of some _named_ class ':m'.

But in eq.(2), 'm' does not stand for some named class, but is a _bound_
variable within the class expression. Now, I do not see any possibility
in OWL-Full to do something like using named bound variables, like 'm'
in eq.(2). Does anybody has a clue how to define the Cantor set in
OWL-Full?

Or, perhaps, it might come out that this isn't possible at all? As far
as I understand, for being undecidable, it is demanded that there is no
single algorithm, which for every pair of ontologies O1 and O2 correctly
states if O1 entails O2, or not. Sounds like that there must at least
/exist an answer/ (either "true" or "false"), which simply is /not
computable/. But in my example above, there /doesn't even exist/ any
answer to the question "C IN C?".

Any ideas, to bring some light to my question?

Cheers,
Michael