RE: Minor bug in http://www.w3.org/TR/owl-semantics/rdfs.html#5.2

Hi Jeremy!

Jeremy Carroll wrote:

>The OWL Full semantics entail that
>OWL:Nothing rdf:type rdfs:Datatype

You are right, I can see it! :) (See attachment below.)

>and similarly for any empty class.
>I believe this is unintentional,

I concur. And this *might* even lead to problems in certain situations, I am
not sure.

>and can be fixed by the addition of
>"n >= 1" in the first of the "Further conditions on owl:oneOf" in the
>reference section.

Looks like the right solution to me. The case of an empty list / set will then
lead to an empty /class/.

Doing so won't conflict with the notion of an empty /datatype/, it is just
less specific: The resulting empty class may still have models which interpret
this class to be a datatype, this only cannot be entailed anymore. So
explicitly defining an empty datatype will /not/ lead to an inconsistent
ontology:

  :D rdf:type rdfs:Datatype
  :D owl:equivalentClass owl:Nothing

Btw: It is still true that a class, which has the empty set as its
class extension, is a /subClassOf/ rdfs:Literal:

  CEXT_I(S_I(owl:Nothing)) = {} SUBSET LV_I = CEXT_I(S_I(rdfs:Literal))

>Jeremy

I will add a Full-TF issue (you as author, I as scribe :)).

Cheers,
Michael


Attachment: owl:Nothing rdf:type rdfs:Datatype
----------------------------------------------

By the IFF semantics of owl:oneOf in the "Conditions on OWL vocabulary
related to boolean combinations and sets" table:

  1) "If x in C_l ...":

     in our case: S_I(owl:Nothing) in C_l

  2) "... and y is a sequence of y1...yn over [...] LV_I ...":

     in particular the empty list S_I(rdf:nil) of data values,
     which is produced by the second comprehension principle
     [FIXME: Do the list comprehension principles produce /empty/ lists?]

  3) "... and CEXT_I(x) = {y1...yn} ..."

     in our case: CEXT_I(S_I(owl:Nothing)) = {}

  4) "... then <x,y> in EXT_I(S_I(owl:oneOf))"

     our intermediate result:
     <S_I(owl:Nothing), S_I(rdf:nil)> in EXT_I(S_I(owl:oneOf))

And then with the first of the "Further conditions on owl:oneOf":

  5) "if l is a sequence of y1...yn over LV_I"

     that's our empty list

  6) "... then if <x,l> in EXT_I(S_I(owl:oneOf))"

     so this matches our intermediate result above:
     <S_I(owl:Nothing), S_I(rdf:nil)> in EXT_I(S_I(owl:oneOf))

  7) "... then x in IDC"

     aha: S_I(owl:Nothing) in IDC
     where "IDC" is the name of the class extension of rdfs:Datatype

Hence, by applying the IFF-style RDFS-semantics of rdf:type :

   owl:Nothing rdf:type owl:Datatype