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

**Problem 19. ** Prove

**Problem 20. ** Prove

**Problem 21. ** Prove

**Problem 22. ** Prove

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: