RE: Layering bug

I don't see this as a problem for OWL DL.
OWL DL (like FOL) does allow you to *assert* that the universe is empty
(for example by saying that "owl:thing equivalentClass owl:Nothing". In
FOL you would say forAll x (x != x)).
There is no harm in this, apart from making your ontology or theory
However, the "Model Theory" of OWL DL (like the MT of FOL) insists that
the universe is non-empty.
This is standard Tarski-style semantics in which only non-empty models
are considered. If an ontology cannot be interpreted in a non-empty
domain, then it is inconsistent and every statement is vacuously
provable in an unsatisfiable theory.

Mehrdad Omidvari

-----Original Message-----
From: pat hayes [] 
Sent: 02 July 2003 21:20
Subject: Re: Layering bug

Coming rather late to this discussion, I am surprised that OWL DL 
allows one to assert that the universe is empty. This would not 
normally be considered to be a consistent assertion in first-order 
logic (it would in a free logic, but free logics have other 
unintuitive properties). Allowing the universe to be empty means that 
assertions like

(forall (?x) (P(?x) and not P(?x)))

are consistent, since they are true in an interpretation with an 
empty universe. In fact, any universal assertion is true in such an 
interpretation, even (forall (?x) False). Is this really what one 
wants to have in OWL DL? It plays havoc with most proof systems for 
conventional logics, and would mean that OWL DL could not be 
translated into a conventional logical notation in a conventional way.

IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell

Received on Thursday, 3 July 2003 05:58:36 UTC