|
|
|---|
|
|
|
|---|
Recursion and Induction: Terms as Formulas
Logicians typically make a careful distinction between terms (whose values range over objects in the domain, like the integers, etc.) and formulas (whose values range over the truthvalues). We have set up two systems of propositional calculus. At the level of formulas we have the traditional equality relation, =, and the logical operators ∧, ∨, ¬, →, and ↔. At the level of terms, we have the primitive function equal and the defined propositional functions and, or, not, implies, and iff. In our term-level propositional calculus, t and nil play the role of truthvalues. Because terms can be written entirely with ASCII symbols (and easily entered on a keyboard!) we tend to write terms and use them as formulas.
For example, we might say that
(implies (and (consp x)
(not (consp y)))
(not (equal x y)))
is a theorem, or even say
((consp x) ∧ ¬(consp y)) → x ≠ y
is a theorem.
But of course, the former cannot be a theorem because it is a term and only formulas are theorems, and the latter cannot be a theorem because it is not even a well-formed formula (it uses some terms as though they were formulas).
If we use an ACL2 term p as though it were a formula then the term should be understood as an abbreviation for the formula p ≠ nil. Thus, if we say term p is a theorem we mean it is a theorem that p is not nil.
Since we assume the reader here is familiar with programming, we assume this
isomorphism between one syntactic category and another is very familiar. If
this makes sense to you, we suggest you just skip the rest of this section,
including the problems below, and go to
This abuse of terminology is justified by the following theorems.
Theorem. NOT is Logical Negation:
(not p) ≠ nil ↔ ¬ (p ≠ nil).
Proof. We handle the two directions of the ↔.
Case 1.
(not p) ≠ nil → ¬ (p ≠ nil).
This is equivalent to its contrapositive:
p ≠ nil → (not p) = nil.
By the definition of not and Axiom 2 and the hypothesis p≠ nil, (not p) = (if p nil t) = nil.
Case 2.
¬ (p ≠ nil) → (not p) ≠ nil.
The hypothesis is propositionally equivalent to p = nil. By substitution of equals for equals, the conclusion is (not nil) ≠ nil. By the definition of not and Axioms 3 and 1, (not nil) = (if nil nil t) = t ≠ nil.
Q.E.D.
Problem 18.
Prove
(and p q) ≠ nil ↔ (p ≠ nil) ∧ (q ≠ nil).
Problem 19.
Prove
(or p q) ≠ nil ↔ (p ≠ nil) ∨ (q ≠ nil).
Problem 20.
Prove
(implies p q) ≠ nil ↔ (p ≠ nil) → (q ≠ nil).
Problem 21.
Prove
(iff p q) ≠ nil ↔ (p ≠ nil) ↔ (q ≠ nil).
Problem 22.
Prove
(equal x y) ≠ nil ↔ (x = y)
Note that these theorems allow us to change the propositional functions to their logical counterparts as we move the “≠ nil” into the term. Furthermore, we can always drop a “≠ nil” anywhere it occurs in a formula since the term with which it appears would then be used as a formula and would mean the same thing.
Problem 23.
Using the theorems above, prove that
(implies (and p (implies q r))
s)
is equivalent to
(p ∧ (q → r)) → s
which is equivalent to
((p ∧ ¬ q) → s) ∧ ((p ∧ q ∧ r) → s)
When writing proofs on paper or the board, we tend to use formulas and the short symbols =, ∧, ∨, ¬, →, ↔ instead of the longer term notation.
Problem 24.
Prove
(equal (car (if a b c)) (if a (car b) (car c)))
that is, prove (car (if a b c)) = (if a (car b) (car c))
Problem 25.
Prove
(equal (if (if a b c) x y)
(if a (if b x y) (if c x y)))
Problem 26.
Prove
(equal (tree-copy (cons a b))
(cons (tree-copy a) (tree-copy b)))
Next: