Re: empty Thing (was Re: proposal to approve tests)

On October 29, Jeremy Carroll writes:
> 
> > > Thing-001       (unless Ian wants us to hold off still)
> 
> > I do. I would like to change the semantics of OWL DL/Lite so that it
> > requires the domain to be non-empty. According to my reading of the
> > OWL Full and RDF semantics, this should already be the case for OWL
> > Full, and so as well as being more consistent with standard DL and FO
> > semantics, it would also fix a mis-match between DL/Lite and Full
> > semantics.
> 
> 
> OWL Full requires Thing to be infinite ...

OK - I forgot how crazy the world is.

> 
> if in contrast you want Thing to be at least n-elements big (with perhaps n = 
> 1) then
> 
> EnumeratedClass( owl:Thing, uri-1, uri-2, .... uri-n )
> 
> is a small test case that exercises this difference between DL and Full.
> (consistent in DL, inconsistent in Full)

This doesn't seem to be in OWL DL, so it is only an example of
something that is syntactically invalid in DL but OK in full.


> The current situation, with n=0, permits small examples that exhibit this 
> difference. Also in OWL DL 0 is already a special number, 1 less so.
> 
> Summary,
>    if you propose an infinite Thing I would support it, despite the lateness 
> of the change. I don't much like any finite number but zero is better than 
> one, and also the change seems insufficiently motivated at this point - since 
> the alignment with Full is specious.

I withdraw the argument about Full. 

The case where an ontology forces Thing to be empty is clearly a
special case, and we have to decide whether such an ontology should be
considered consistent. There are good reasons why it should NOT be
considered consistent (the standard treatment in DL and FOL):

- If such an ontology is consistent, then the axiom A implies not A is
consistent.

- If such an ontology is consistent, then we can have a situation
where all classes, including Thing, are inconsistent, yet the ontology
is still consistent (unfortunately we don't explicitly state in our
documents what it means for a class to be consistent w.r.t. an
ontology, but the standard definition is that there is some model of
the ontology in which the class has a non-empty extension).

- If such an ontology is viewed as a FO theory, then the theory
entails false.

- If such an ontology is viewed as a DL knowledge base, then the KB is
inconsistent.


If we want such ontologies to be considered inconsistent, as I am
arguing, then the easiest (and standard) way is simply to change the
definition of what constitutes a model (by insisting that the universe
be non-empty). This would involve minimal changes to the S&AS document
and a change to one test case.

Ian



> 
> Jeremy
> 
> 
> 
>

Received on Wednesday, 29 October 2003 18:39:47 UTC