In statements of theorems, we conventionally use letters f, g, and h to represent functions that return values that are not boolean. Letters p and q are used for predicates, in other words functions with boolean values.

Axiom 2 and axiom 3 are shown in two forms. The second form shows their functional parameters (f, g, h) as predicates (p, q), for the case where their values are boolean.

~~1) p T & p F == forall {a. p a}
2a) x = y => h x = h y
2b) x = y => (p x == p y)
3a) (f = g) == forall {x. f x = g x}
3b) (p = q) == forall {x. p x == q x}
4) {x. R} S = R[x := S]
5) the1 {x. x = y} = y
6) if T x y = x
7) if F x y = y~~

In the description of Axiom 4, the notation R[x := S] means the result
of properly substituting `S`

for `x`

in `R`

. Proper substitution only
replaces occurrences of `x`

that are free in the “body” (`R`

). We say
that `{x. R}`

binds the variable `x`

, and that `x`

is bound in
`{x. R}`

. If R contains any bound variables, substitution in
Prooftoys may also automatically rename them to avoid a phenomenon
known as “capture”. See the technical notes for more details.

This process of converting `{x. R} S`

to an equivalent term via proper
substitution is known as “beta conversion”.

Definitions including all of those used in the theorems list below. Some additional definitions are used internally or in theorems about real numbers.

All of these definitions have the form `<name> = <expression>`

and meet the
additional requirements for being safe definitions that cannot introduce
contradictions into the logic.

Definitions of functions and predicates in this list are given in pairs; first the native form with only the name of the new constant on the left, and then in the traditional form. The two forms are equivalent. See the inference rules for unbinding and rebinding equations.

For more on the use of definitions in Prooftoys see the definitions page.

~~not = {a. a == F}
not a == (a == F)~~

~~(&) = {a. {b. if a b F}}
a & b == if a b F~~

~~(|) = {a. {b. if a T b}}
a | b == if a T b~~

~~(=>) = {a. {b. if (not a) T b}}
a => b == if (not a) T b~~

~~forall = {p. p = {x. T}}
forall p == p = {x. T}~~

~~(!=) = {x. {y. not (x = y)}}
x != y == not (x = y)~~

~~exists = {p. p != {x. F}}
exists p == p != {x. F}~~

~~exists1 = {p. exists {x. p = {y. y = x}}}
exists1 p == exists {x. p = {y. y = x}}~~

~~ident = {x. x}
ident x = x~~

~~multi = {p. exists {x. exists {y. p x & p y & x != y}}}
multi p == exists {x. exists {y. p x & p y & x != y}}~~

~~empty = {x. F}
none = the1 empty~~

There is also a “live” display of all of these theorems collected on a page here. It shows each theorem, with access to a rigorous proof verified by Prooftoys.

Equality:
~~(x = y) == (y = x)
x = y & y = z => x = z~~

Functions ("eta conversion")
~~{x. p x} = p~~

All tautologies can be proved, as described here and here.

Here is a list of some tautologies that are used in Prooftoys or may
be useful in building your own proofs. Remember that all uses of `==`

can be reversed because of the symmetry of equality.

The comments suggest places where you may see these tautologies in Prooftoys proofs.

~~a == a~~ (the "consider" rule)
~~a => a~~ (the "assume" rule)
~~(a == b) == (b == a)~~ (symmetry of equality/equivalence)
~~a == (a == T)~~ (replacing a theorem with ~~T~~ or ~~T~~ with a theorem)
~~a & T == a~~

Relating "and" and "or":
~~not (a & b) == not a | not b~~
~~not (a | b) == not a & not b~~

Conditionals:
~~(T => a) == a~~
~~(a => F) == not a~~ (proofs by contradiction)
~~(a => b) & (b => c) => (a => c)~~ ("forward" reasoning)
~~(a => b) & (b => a) == (a == b)~~ (proofs of equivalence)
~~(a => b) == (not b => not a)~~
~~(a => (b => c)) == (a & b => c)~~ (managing assumptions)

Unlike first-order logic, in some of these theorems
are terms such as `forall p`

. Where they
exist in the list below, you can read them as for example
`forall {x. p x}`

using eta conversion if you prefer.

In this group of quantifier laws, terms such as `p x`

or `p x y`

inside quantifiers allow the rule to apply to any boolean term. We
will discuss the reasons for this in a more advanced section, but be
reassured that you can apply these theorems easily, and Prooftoys will
take care of the technical details for you.

Simple quantifier rearrangement:
~~forall {x. forall {y. p x y}} == forall {y. forall {x. p x y}}
exists {x. exists {y. p x y}} == exists {y. exists {x. p x y}}~~

Relationship between "forall" and "exists"
~~forall p == not (exists {x. not (p x)})
exists p == not (forall {x. not (p x)})~~

Reasoning with instances:
~~forall p => p x
p x => exists p~~

For more, see also the “live” list of logic theorems and the advanced quantifier laws.