|
|
|---|
|
|
|
|---|
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:
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)) ≠ nil Proof.
| 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
Axiom tree-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: