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

Re: Layering bug

From: pat hayes <phayes@ihmc.us>
Date: Wed, 2 Jul 2003 15:19:44 -0500
Message-Id: <p0600121abb28ecd603de@[10.0.100.7]>
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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:58:01 GMT