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

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.

So, although one can talk about certain ill-formed "sets" in OWL Full,
these sets do not necessarily exist in all semantic structures - in fact
some of them cannot exist in any semanticc structure and so just talking
about them is contradictory.

Peter F. Patel-Schneider


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 Saturday, 4 November 2006 15:06:16 UTC