## Laws for Manipulating Quantifiers

*Binding free variables in a tautology*
If a logical expression L with free variables x1..xn
is a tautology, then (A x1)(A x2)..(A xn) L is also a tautology.

We can use the above rule to bind all free variables
in a tautology to a universal quantifier.

P(x,y) OR NOT P(x,y) == 1
== (A x)(A y) (P(x,y) OR NOT P(x,y))

An expression with no free variables is a
*closed* expression.

*Moving NOT within a quantifier*

There is rule analogous to DeMorgan's law that allows us to
move a NOT operator through an expression containing a quantifier.

NOT (A x) L(x) == (E x) (NOT L(x))
NOT (E x) L(x) == (A x) (NOT L(x))

The first rule can be read as "it is not the case that for all x,
L(x) is true" is equivalent to "for some x, it is not the case
that L(x) is true".
The second rule can be read as "it is not the case that for some x
L(x) is true" is equivalent to "for all x, it is not the case
that L(x) is true".

*Moving quantifiers through AND and OR*

L1 AND (A x) L2(x) == (A x) (L1 AND L2)
L1 AND (E x) L2(x) == (E x) (L1 AND L2)
L1 OR (A x) L2(x) == (A x) (L1 OR L2)
L1 OR (E x) L2(x) == (E x) (L1 OR L2)

Note that we require x is not a free variable in expression L1
in the above rules.
We may have to rename variable x (consistently) in L2 to avoid
any overlap with free variables in L1.

### Manipulating Quantifiers: Example

Given the following expression:

(A x)P(x) OR (E x)(NOT P(x))

we can rename the second occurrence of x to avoid any overlap
with the first occurrence and arrive at the equivalent expression
(A x)P(x) OR (E y)(NOT P(y))

Moving the universal quantifier through the OR we arrive at
(A x) (P(x) OR (E y)(NOT P(y)))

Moving the existential quantifier through the OR we arrive at
(A x) (E y) (P(x) OR NOT P(y))

Using these rules, we can write any expression involving
quantifiers Q1, Q2, .. QN,
and the logical operators AND, OR, and NOT
in *prenex* form:

(Q1 x1)(Q2 x2)..(Qn xn)L

where all the quantifiers appear outside expression L.
- First, rewrite the expression so that all of the quantifiers
refer to distinct variables not found in other quantifiers or free
in the expression.
- Use the rules above to move the quantifiers outside NOT, AND,
and OR.