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 formforall {x. p x & q x} == forall p & forall q
exists {x. p x | q x} == exists p | exists qOne-way rearrangements:
forall p | forall q => forall {x. p x | q x}
exists {x. p x & q x} => exists p & exists qUnused 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 qUnique 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)forall {x. p x & q x} == forall {x. p x} & forall {x. q x}
exists {x. p x | q x} == exists {x. p x} | exists {y. q y}One-way rearrangements:
forall {x. p x} | forall {x. q x} => forall {x. p x | q x}
exists {x. p x & q x} => exists {x. p x} & exists {x. q x}Unused bound variable:
forall {x. A} == A
exists {x. A} == A
forall {x. A | q x} == (A | forall {x. q x})
forall {x. A => q x} == (A => forall {x. q x})
exists {x. A & q x} == A & exists {x. q x}
forall {x. p x => A} == (exists {x. p x} => A)Forward reasoning:
forall {x. p x => q x} => (forall {x. p x} => forall {x. q x})
forall {x. p x => q x} => (exists {x. p x} => exists {x. q x})Unique existence:
exists1 {x. p x} == exists {x. p = {y. y = x}}
exists1 {x. p x} == exists {x. forall {y. p y == y = x}}
exists1 {x. p x} == exists {y. p y & forall {z. p z => z = y}}
exists1 {x. p x} => (p x == x = the1 p)
p x & forall {y. p y => y = x} => exists1 {x. p x}
(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.