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.
1. First, rewrite the expression so that all of the quantifiers refer to distinct variables not found in other quantifiers or free in the expression.
2. Use the rules above to move the quantifiers outside NOT, AND, and OR.