W3C home > Mailing lists > Public > www-webont-wg@w3.org > July 2003

RE: Layering bug

From: pat hayes <phayes@ihmc.us>
Date: Thu, 3 Jul 2003 09:49:30 -0500
Message-Id: <p06001235bb29f2a1ccb1@[]>
To: "Mehrdad Omidvari" <Mehrdad.Omidvari@networkinference.com>
Cc: <www-webont-wg@w3.org>

>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

As I understand the current exchange, the claim is that this 
assertion is *consistent* in OWL-DL; hence my message.


>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 [mailto:phayes@ihmc.us]
>Sent: 02 July 2003 21:20
>To: www-webont-wg@w3.org
>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
>phayes@ihmc.us       http://www.ihmc.us/users/phayes

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
phayes@ihmc.us       http://www.ihmc.us/users/phayes
Received on Thursday, 3 July 2003 10:49:33 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:54 UTC