------------------------------------------------------------------------
Subject:  Negating Nested Quantifiers
------------------------------------------------------------------------

Here are some comments on negating nested quantifiers that you might
find helpful.

Consider this proposition:

	Ax[P(x) -> Ey[R(y) ^ Q(x,y)]]

For a slightly more realistic example, suppose we have the following
semantics for these predicates:

P(x)   = x is an integer
R(y)   = y is a negative integer
Q(x,y) = x > y

Then our proposition represents the English sentence:

	For all x, if x is an integer,
	           then there is a y such that y is a negative integer
	                                       and x > y

or, more idiomatically,

	Any integer is greater than some negative integer.

(Hopefully, you believe that!)


Let's try to negate this.  In what follows, I'll use "equiv" for "is
logically equivalent to" (i.e., for the triple bar symbol).

-Ax[P(x) -> Ey[R(y) ^ Q(x,y)]]
	equiv
Ex-[P(x) -> Ey[R(y) ^ Q(x,y)]], because -Axp equiv Ex-p
	equiv
Ex-[-P(x) v Ey[R(y) ^ Q(x,y)]], because (p -> q) equiv (-p v q)
	equiv
Ex[--P(x) ^ -Ey[R(y) ^ Q(x,y)]], by DeMorgan
	equiv
Ex[P(x) ^ -Ey[R(y) ^ Q(x,y)]], by DN
	equiv
Ex[P(x) ^ Ay-[R(y) ^ Q(x,y)]], because -Exp equiv Ax-p
	equiv
Ex[P(x) ^ Ay[-R(y) v -Q(x,y)]], by DeMorgan

We could stop here, but let's go one step further to make it a bit
easier to express in English:

The previous proposition is logically equivalent to:
Ex[P(x) ^ Ay[R(y) -> -Q(x,y)]], because (p -> q) equiv (-p v q)

This says:

	There is an x such that x is an integer
	                        and, for all y,
	                             if y is a negative integer,
	                             then x is not > y

or, more idiomatically, using "<=" for "is less than or equal to"
(which is the negation of ">")

	some integer <= all negative integers

(Hopefully, you don't believe that!)