Substitution Proofs of Arithmetic Equations

We describe an alternative notion of proof, called a substitution proof, for arithmetic equations.

Figure 1 in the Notes on Proving Arithmetic Equations (pdf) listed a formal proof consisting of a sequence of equations and ending with the equation

(f + g) + -g = f.

Another style of proof for this equation is the sequence of equalities

(f + g) + -g = f + (g + -g) = f + 0 = 0 + f = f. Here the first equality follows from (associativity), the second from (inverse for +), and the third and fourth by (symmetry) and (identity for +), respectively. Proofs in this format are attractive and easy to follow because each equality follows solely from the immediately previous equality by substituting equals for equals -- in contrast to the sequence-of-equations proofs of the Notes, where justification of an equation may require appeal to more than one antecedent.

Here is a precise definition of such substitution proofs:

Definition. An arithmetic substitution proof is a sequence of ae's, e_i, separated by equality symbols: e₁ = e₂ = e₃ = ...= e_n such that for 1 ≤ i < n, the expression e_i+1 is obtained from e_i by substituting equals for equals. Namely there is an ae, h_i, with exactly one occurrence of some variable, x, and there is an axiom instance, (f_i = g_i), such that the expressions e_i and e_i+1 are the same as the expressions h_i[x:=f_i] and h_i[x:=g_i] (in either order). The equation proved by the proof is (e₁ = e_n).

Problem 1. Define a Scheme procedure

tree-proof-->subst-proof that transforms a tree proof corresponding to the recursive definition of Arithmetic Equational Theorems (aet's) given in the Notes (pdf) into a substitution proof of the same equation. For input to the procedure, the tree proof will be represented in the usual way as a Scheme list structure (see below). You should turn in (preferably by email) your procedure definitions and some sample output indicating that the procedure works properly.

In designing the Scheme procedure tree-proof-->subst-proof, we assume for simplicity that an equational proof as defined in the Notes will be represented as a tree showing the antecedents and rule used to arrive at each equation in the proof. For example, the proof in Fig.1 of the Notes, would be represented in tree form as:

               reflexivity            inverse-for+
                  (f=f)              ((g + (- g)) = 0)
                    \                      /
                      \ congruence-for+  /
                        \              /
                         \            /                 commutativity-for+
                    ((f + (g + (- g))) = (f + 0))       ((f + 0) = (0 + f))
                                   \                            /
                                       \       transitivity    /
                                           \                 /
          associativity                      \              /
(((f + g) + (- g)) = (f + (g + (- g))))    (((f + (g + (- g))) = (0 + f))
          \                                           /
           \                                        /
            \                                     /
             \        transitivity              /
              \                               /
               \                            /
                \                         /                 identity-for+
            (((f + g) + (- g)) = (0 + f))                   ((0 + f) = f)
                            \                                    /
                               \                               /
                                  \      transitivity        /
                                    \                      /
                                     \                    /
                                     (((f + g) + (- g)) = f)

This tree would then be represented as a Scheme list structure. Namely, the proof is represented as a list of the equation proved, a token indicating the inference rule by which it was deduced, and, if the inference rule was not an axiom, the lists representing the proofs of the antecedents of the inference rule. So the representation of the proof tree above would be:

(define Fig1-tree-proof
  '((((f + g) + (- g)) = f)
      transitivity
      ((((f + g) + (- g)) = (0 + f))
         transitivity
         ((((f + g) + (- g)) = (f + (g + (- g)))) associativity-of+)
         (((f + (g + (- g))) = (0 + f))
            transitivity
            (((f + (g + (- g))) = (f + 0))
                congruence-for+
                ((f = f) reflexivity)
                (((g + (- g)) = 0) inverse-for+))
            (((f + 0) = (0 + f)) commutativity-for+)))
      (((0 + f) = f) identity-for+)))

Now applying the procedure to this input might produce the following printout:

(tree-proof-->subst-proof Fig1-tree-proof)
;Value: (((f + g) + (- g)) = (f + (g + (- g))) = (f + 0) = (0 + f) = f)

This proof-transforming procedure shows that the class of equations provable by substitution proofs is at least as large as the equations provable using the tree proofs for aet's. Since we've already argued that the sequence-of-equations proof system is complete and that the tree-proofs are interconvertible with sequence-of-equations proofs, we can conclude that the substitution proof system indeed also proves all the valid equations. But since substitution proofs are sound (see below), it follows that they prove exactly the valid equations. That is, substitution proofs are another complete proof system for arithmetic equations.

Problem 2. Consider the following variations of the substitution rules for equality, adapted for inequalities:

(f ≤ g) ⇒⇒ (e[x:=f] ≤ e[x:=g])
(f ≤ g) ⇒⇒ (f[x:=e] ≤ g[x:=e])

Only one of these rules preserves validity. Give a simple example of arithmetic expressions e,f,g where one of these rules fails to preserve validity. Prove that the other rule does preserve it.

This document last modified