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 “there exists exactly one” (or “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 within {x. . . . } capture the same idea as informal notations such as ∀ x. φ(x) found in some textbooks.

Quantifier laws

Prooftoys form

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} & forall p => forall q forall {x. p x => q x} => (exists p => exists 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.