Re: Undecidability of OWL-Full and Cantor's antinomy

Peter F. Patel-Schneider wrote on 2006-11-04:

> I believe that you are going down the wrong path here.
> 
> Your argument goes more towards semantic paradox than decidability.  If the
> bad set was present in all OWL Full semantic structures, then the meaning
> of OWL Full would collapse.  However, OWL Full was carefully engineered to
> avoid many of the common semantic paradoxes, and thus only certain kinds of
> "sets" are present in all OWL Full semantic structures.

Aha, I did not know this! Until now, I had in mind some vague concept of 
the form "in OWL-Full I can express whatever I want", and that it would 
be up to me to not write down nonsense (like I actually /can/ write down 
this Cantor's set in mathematics, because it is /syntactically/ a well 
formed expression, but, as I understand it, it simply does not have any 
meaning in mathematics).

In most cases, when thinking about some distinctive difference between 
OWL-Full and DL, I had in mind this

   owl:Class rdf:type owl:Class .

triple, which means that in OWL-Full a class can be an instance of 
itself. And if this is allowed, than the following should also be allowed:

   owl:Class rdf:type [ owl:complementOf owl:Class ] .

and this, as you might guess, finally took me to the idea of defining 
the "bad" Cantor set.

But, ok, from what you said this probably won't work, and this is, of 
course, a good thing. :)

Thanks for your reply!

Michael


> From: "Michael Schneider" <m_schnei@gmx.de>
> Subject: Undecidability of OWL-Full and Cantor's antinomy
> Date: Fri, 3 Nov 2006 18:01:26 -0600
> 
>> 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
>>

Received on Tuesday, 7 November 2006 09:36:50 UTC