Recursion and Induction: Axioms

A formal mathematical theory is given by a formal syntax for *formulas*, a
set of formulas designated as *axioms*, and some formula manipulation
*rules of inference*
that allow one to derive *new* formulas from *old* ones. A *proof* of
a formula *p* is a derivation of *p* from the given axioms using the given
rules of inference. If a formula can be proved, it is said to be a
*theorem*. Formulas are given *semantics* similar to those described for
terms. Given an *assignment* of values to variable symbols and an
interpretation of the function symbols, every formula is given a truthvalue
by the semantics. Given an interpretation, a formula is *valid* if it is
given the value true under every possible assignment to the variable symbols.
A *model* of a theory is an interpretation that makes all the axioms valid.
Provided the rules of inference are validity preserving, every theorem is
valid, i.e., *always true*.

We assume you know all that, and won't go into it further. The whole point of a practical formal theory is to use proof to determine truth: one way to determine if a formula is true is to prove it.

If *α* and *β* are terms, then *α* = *β* is a
*formula*. If *p* and *q* are formulas, then each of the
following is a formula:

*p*→*q**p*∧*q**p*∨*q*- ¬
*p* *p*↔*q*.

If *α* and *β* are terms, then *α*
≠ *β* is just an
abbreviation for the formula ¬(*α* = *β*).

We extend the notation *term*/*σ* in the obvious way so that we can apply
substitution *σ* to formulas, replacing all the variables bound by
*σ* in all the terms of the formula.

The axioms we will use for the initial part of our study are given below. Note that Axioms 1 and 8 are actually axiom schemas, i.e., they describe an infinite number of axioms.

Axiom |
1. |
'α ≠ 'β, |

where α and β are distinct integers, characters, strings, or symbols |
||

Axiom |
2. |
x ≠ nil → (if x y z) = y |

Axiom |
3. |
x = nil → (if x y z) = z |

Axiom |
4. |
(equal x y) = nil ∨ (equal x y) = t |

Axiom |
5. |
x = y ↔ (equal x y) = t |

Axiom |
6. |
(consp x) = nil ∨ (consp x) = t |

Axiom |
7. |
(consp (cons x y)) = t |

Axiom |
8. |
(consp 'α) = nil, |

where α is an integer, character, string, or symbol |
||

Axiom |
9. |
(car (cons x y)) = x |

Axiom |
10. |
(cdr (cons x y)) = y |

Axiom |
11. |
(consp x) = t → (cons (car x) (cdr x)) = x |

Axiom |
12. |
(consp x) = nil → (car x) = nil |

Axiom |
13. |
(consp x) = nil → (cdr x) = nil |

One axiom described by Axiom (schema) 1 is `'t` ≠ `'nil`. Others
are `'nil` ≠ `'3` and `'"Hello"` ≠ `'Hello`.
We refer to all of these as Axiom 1.

One axiom described by Axiom (schema) 8 is `(consp 'nil)` = `nil`.
Others are `(consp '3)` = `nil` and `(consp 'Hello)` =
`nil`. We refer to all of these as Axiom 8.

Note that if *φ* is an axiom or theorem and *σ* is a substitution,
then *φ*/*σ* is a theorem, by the Rule of Instantiation.

We assume you are familiar with the rules of inference for propositional calculus and for equality. For example, we take for granted that you can recognize simple proposititional tautologies, reason by cases, and substitute equals for equals.

For example, we show a theorem below that you should be able to prove, using nothing but your knowledge of propositional calculus and equality (and Axiom 1).

The proof shown below uses the Deduction Law of propositional calculus: we can
prove *p* → *q* by assuming *p* as a
“Given” and deriving *q*.

Theorem.(consp x) = t ∧ x = (car z) → (consp (car z)) ≠ nilProof.

1. | (consp x) = t |
{Given} |
||

2. | x = (car z) |
{Given} |
||

3. | t ≠ nil |
{Axiom 1} |
||

4. | (consp x) ≠ nil |
{Equality Substitution, line 1 into line 3} |
||

5. | (consp (car z)) ≠ nil |
{Equality Substitution, line 2 into line 4} |
||

Q.E.D. |

We will not write proofs in this style. We will simply say that the formula is a theorem “by propositional calculus, equality, and Axiom 1.”

Recall that each function definition adds an axiom. The definition

(defun tree-copy (x) (if (consp x) (cons (tree-copy (car x)) (tree-copy (cdr x))) x))

adds the axiom

Axiomtree-copy (tree-copy x) = (if (consp x) (cons (tree-copy (car x)) (tree-copy (cdr x))) x)

Thus, by the Rule of Instantiation

Theorem.(tree-copy (cons a b)) = (if (consp (cons a b)) (cons (tree-copy (car (cons a b))) (tree-copy (cdr (cons a b)))) (cons a b))

Next: