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)
|