- From: pat hayes <phayes@ihmc.us>
- Date: Wed, 2 Jul 2003 15:19:44 -0500
- To: www-webont-wg@w3.org
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 Wednesday, 2 July 2003 16:19:48 UTC