# Advanced quantifier laws

These are mostly needed for more advanced proofs, especially proofs of existence, with the existential quantifier. A handful of simple number facts have quantifiers, but their proofs don’t need these quantifier laws.

These laws all contain quantifiers, `forall`, `exists`, or `exists1` for “unique existence”. A few also use `the1`, which gives the unique value satisfying a condition, if there is indeed exactly one such value.

Uses here of `p x` capture the same idea as informal notations such as `∀ x. phi(x)` found in some textbooks.

Rearrangement: forall {x. p x & q x} == forall p & forall q exists {x. p x | q x} == exists p | exists q
One-way rearrangements: forall p | forall q => forall {x. p x | q x} exists {x. p x & q x} => exists p & exists q
Unused bound variable: forall {x. A} == A exists {x. A} == A forall {x. A | q x} == (A | forall q) forall {x. A => q x} == (A => forall q) exists {x. A & q x} == A & exists q forall {x. p x => A} == (exists p => A)
Forward reasoning: forall {x. p x => q x} => (forall p => forall q) forall {x. p x => q x} => (exists p => exists q)
Unique existence: exists1 p == exists {x. p = {y. y = x}} exists1 p == exists {x. forall {y. p y == y = x}} exists1 p == exists {y. p y & forall {z. p z => z = y}} exists1 p => (p x == x = the1 p) p x & forall {y. p y => y = x} => exists1 p (f x = the1(Q x) & exists1 (Q x)) => (Q x y == f x = y)

### Using the laws

The proof builder will offer these laws when they apply to a term you select. Still, to understand how to use them takes a bit more than other parts of Prooftoys.

In many of these laws there is at least one occurrence of a term like `p x`, where `p` is a free variable and `x` is bound somewhere in the statement.

Also, in some of the theorem statements there are occurrences of the variable `A` in the scope of a bound variable. In a form such as `forall {x. A}`, it is not possible to substitute for `A` in a way that puts the bound variable `x` into that part of the result. Proper substitution automatically renames the `x` in `forall {x. A}` to something else if `x` is free in the term that replaces `A`, so the substitution fails to put an occurrence of the bound variable into the result.

On the other hand, in a form such as `forall {x. p x}`, substitution can turn the `p x` into any term with a true/false value.

For example `p x` can become `x + 0 = x`, though it does not look like it. The trick is to substitute for `p` and then do a beta conversion (axiom 4). Here `x + 0 = x` is equivalent to `{z. z + 0 = z} x`. So substituting `{z. z + 0 = z}` for `p` and then using beta conversion (also a form of substitution, see above) results in `x + 0 = x` as desired. In fact there is no need to change `x + 0 = x` to ```z + 0 = z```. Even `{x. x + 0 = x}` works fine and is slightly simpler, though it may make the step a bit harder to read.

There are even more theorems like this, many dealing with specific issues in reasoning, but these classic laws are implemented in Prooftoys today.