ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] Validity of laws of predicate logic under CWA and NA

 To: ankesh@xxxxxxxxx, "[ontolog-forum]" Ed Barkmeyer Fri, 20 Feb 2009 12:48:38 -0500 <499EECF6.3040708@xxxxxxxx>
 Ankesh Khandelwal wrote:    (01) > I have a knowledge base and a set of rules written under closed world > assumption that use negation only as negation as failure. > > Under these circumstances are the laws of quantifier movement valid?    (02) As Adrian points out, you must be clear about your 'closed world' and NAF semantics. Let 'not P(x)' mean 'P(x) is not entailed (by the existing KB)', 'all x' mean 'all known x' and 'exists x' mean 'exists a known x'. And assume that the set of all x's is finite and non-empty.    (03) > Laws of Quantifier movements: > 1. '(all x.P(x)) --> Q' equivalent-to 'exists x.(P(x)-->Q)', provided x is > not free in Q    (04) I don't believe this axiom. I read it to say, for example, "if all the players are present, the match can begin" is equivalent to "there is at least one player whose presence (alone) will allow the match to begin"    (05) The implication is correct only in one direction: exists x.(P(x) --> Q) implies (all x.P(x)) --> Q If there is a player whose presence allows the match to begin, then if all the players are present, the match can (surely) begin.    (06) > 2. '(exists x.P(x)) --> Q' equivalent-to 'all x.(P(x)-->Q)', provided x > is not free in Q > 3. 'P --> (all x.Q(x))' equivalent-to 'all x.(P --> Q(x))', provided x is > not free in P > 4. 'P --> (exists x.Q(x))' equivalent-to 'exists x.(P --> Q(x))', provided > x is not free in P    (07) These should hold, and you should be able to prove that they hold.    (08) > And/ Or are the following laws valid?    (09) Yes, and you can prove that by induction.    (010) > 1. 'not(all x. P(x))' equivalent-to 'exists x.(not P(x))', where not has > the Negation as Failure semantics.    (011) If there exists a known x for which P(x) cannot be proved, then it is not possible to prove P(x) for all known x. Conversely, if it is not possible to prove x for all known x, then one can examine the set of known x's one-by-one (which requires the Well-Ordering Principle, OK) until we find one for which it cannot be proven. If we exhaust the set without finding one, the antecedent is contradicted.    (012) > 2. 'not(exists x. P(x))' equivalent-to 'all x.(not P(x))', where not has > the Negation as Failure semantics.    (013) If you can't find an x for which P(x) can be proved, then for all x, P(x) cannot be proved. Conversely, if P(x) cannot be proved for all/any known x, then if there were a known x for which P(x) can be proved, it would be a contradiction.    (014) -Ed    (015) -- Edward J. Barkmeyer Email: edbark@xxxxxxxx National Institute of Standards & Technology Manufacturing Systems Integration Division 100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528 Gaithersburg, MD 20899-8263 FAX: +1 301-975-4694    (016) "The opinions expressed above do not reflect consensus of NIST, and have not been reviewed by any Government authority."    (017) _________________________________________________________________ Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/ Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/ Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx Shared Files: http://ontolog.cim3.net/file/ Community Wiki: http://ontolog.cim3.net/wiki/ To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (018)
 Current Thread [ontolog-forum] Validity of laws of predicate logic under CWA and NAF, Ankesh Khandelwal Re: [ontolog-forum] Validity of laws of predicate logic under CWA and NAF, Adrian Walker Re: [ontolog-forum] Validity of laws of predicate logic under CWA and NAF, Ed Barkmeyer <= Re: [ontolog-forum] Validity of laws of predicate logic under CWA and NAF, Christopher Menzel