# Axioms and theorems of the logic

## Axioms

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

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

Definitions have the form `<name> <vars> = <expression>`

where
`<name>`

is the newly-defined constant and `<vars>`

is an optional
sequence of variable names.

The expression must not have any free variables other than those in the list after the name being defined.

`not a == (a == F)`

`a & b == if a b F`

`a | b == if a T b`

`a => b == if (not a) T b`

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

`x != y == not (x = y)`

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

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

`ident x = x`

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

`empty = {x. F}`

`none = the1 empty`

## Theorems of the logic

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.

### Basic theorems

`(x = y) == (y = x)`

`x = y & y = z => x = z`

Functions (“eta conversion”)

`{x. p x} = p`

### Tautologies

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)`

Managing assumptions:
` (a => (b => c)) == (a & b => c)`

Resolving side conditions, e.g. `a == (x = 0)`

` (not a => (p == b)) & (a => p) => (p == a | b)`

### Some basic quantifier laws

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.

`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.