Consequences of the Standard Form Lemma


The Standard Form Lemma says that any CL-expression can be transformed, using legal moves, into the following standard form:

\[ \dpi{130} E = \prod_{B\in \mathfrak{B}}(B(E_B)) \]

(read as: 'E equals the product over all B in $\mathfrak{B}$ of (B(EB))' ), where $\mathfrak{B}$ is the set of 'basic' expressions using the same letters that occur in E, such as

B = a (b)(c) d...(i) j k ,

and where EB would mean, in this case, the expression that is derived from E by substituting _ for a, O for b, O for c, _ for d, ... O for i, _ for j, _ for k. All the EB's are arithmetic expressions, reducible to either _ or O. In the first case, the corresponding factor in the standard form vanishes; in the second case, it reduces to (B).

First Consequence: If all the EB reduce to _ , then E is equivalent to the empty expression.

Second Consequence: If EB reduces to the same value as FB, for all B, then E is equivalent to F. This amounts to an 'arithmetic test' for the equivalence of any two expressions E and F. For convenience, we will sometimes refer to this consequence as the Test Theorem.

Third Consequence: The axioms of the CL-Calculus are complete, in the following sense: suppose one added a fourth initial equation to the existing three, in the hope of enlarging the set of legal moves. Then either

the new equation is a consequence of the first three

or

the new equation is incompatible with the arithmetic of the mark, i.e. it is possible, by substituting arithmetic values for the letters in the expressions on either side of the new equation, to obtain the equation

O = _ .

There are several ways of seeing that this equation reduces the CL-calculus to triviality, in the sense that all expressions become equivalent to one another. Most directly, if O = _ , then

E = E _ = E O = O = _ ;

so all expressions whatsoever are equivalent to the void. Thus the set of three initial equations cannot be meaningfully expanded, without bringing disaster on the whole enterprise.

Fourth Consequence: any algebraic equation that is valid as a general rule in the algebra of the mark, can be derived as an equivalence in the CL-calculus. The question about which 'initial equations' Aeneas would have to take with him as he fled the ruins of Troy, in order to regenerate all possible general rules, is answered: the three initial equations of the CL-calculus will do.