- From: Mehrdad Omidvari <Mehrdad.Omidvari@networkinference.com>
- Date: Thu, 3 Jul 2003 10:39:45 +0100
- To: "pat hayes" <phayes@ihmc.us>, <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 inconsistent. 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. Pat -- --------------------------------------------------------------------- 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 05:58:36 UTC