- From: pat hayes <phayes@ihmc.us>
- Date: Thu, 3 Jul 2003 09:49:30 -0500
- 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 >inconsistent. As I understand the current exchange, the claim is that this assertion is *consistent* in OWL-DL; hence my message. Pat >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 -- --------------------------------------------------------------------- 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