The 'Case Analysis' LemmaRecall the equation that we have called each way: a = ((ab)(a(b))). In particular, let E be any expression, and let x be any letter occurring in the expression. Then E = ((xE)((x)E)). Now, in the first inner factor, E stands 'in the presence of x', which implies that any instance of x in E may be uncopied out of E. In the second inner factor, E stands in the presence of (x), which implies that any instance of (x) in E may be uncopied out of E. What do we mean by that? Well, any instance of x in E can be replaced by the wrapped form ((x)); when (x) is uncopied what is left is an empty mark, O. So uncopying (x) is the same as replacing each occurrence of x by the mark O. Indeed, returning for a moment to the first inner factor, the removal of any instance of x can also be described as the replacement of x by _ . Let us define two new expressions, derived from E: 1) Ex is defined to be the expression which results, when all instances of x in E are replaced by _ . If by any chance there are not, after all, any occurrences of x in E, that is no problem! In that case, Ex is just E. 2) E(x) is defined to be the expression which results, when all instances of x in E are replaced by O . Note that Ex and E(x) are expressions which do not contain the letter x. By what has been said already, we have the following 'Case Analysis' Lemma: E = ( (xE) ((x)E) ) = ( (xEx) ((x)E(x)) ) . Now E may be a very complicated expression in which the letter x appears many times. We have derived an equivalent form in which x appears just twice: once in the first inner factor, once in the second.[1] Suppose that both Ex and E(x) are found to be void-equivalent (equivalent to the empty expression). Then E = ((x _ ) ((x) _ )) = ((x)((x))) = _ [complements] . If, on the other hand, E is known to be equivalent to the void, then so must Ex and E(x) be. (For the first, just substitute _ for x in both sides of the equation E = _ . For the second, substitute O for x instead.) Thus a necessary and sufficient condition for E to be void-equivalent is that both the derived expressions are void-equivalent. We can apply this to the case when E is the equivalence expression of two other expressions A and B. We note that [A|B]x = [Ax|Bx], and deduce A=B if and only if Ax=Bx and A(x)=B(x) ; in other words, if and only if the expressions are equivalent when _ is substituted for x, and also when O is substituted for x. In a loose way of talking, we could say that the expressions must be equivalent 'when x= _ ', and 'when x = O '; indeed, this is why we call it the 'Case Analysis' Lemma. But note the quotation marks: everything works out AS IF x was a variable that could only take two values, AS IF there were just two cases - but that is nonsense: x is just a letter, nobody ever said anything about x 'taking a value' - or 'taking one of two values'. The Lemma is an unlooked-for boon: it says that equivalence of circle-and-letter expressions can be checked, surprisingly, by checking just two cases: (1) all occurrences of a letter (x, say) replaced by _ (2) all occurrences of x replaced by O. If one knows that Ax is equivalent to Bx, and A(x) is equivalent to B(x), one can see directly that A must be equivalent to B, without appealing to the equivalence expression: A = ((xAx) ((x)A(x))) = ((xBx) ((x)B(x))) = B. Alternative Form of the LemmaSubstituting (E) for E, the Case Analysis Lemma becomes (E) = ((x(E)x)((x)(E)(x))) . But (E)x is just (Ex), and (E)(x) is just (E(x)), so we have (E) = ( (x(Ex)) ((x)(E(x))) ) and consequently, circling both sides of the equation, E = (x(Ex)) ((x)(E(x))) . This is the second, alternative form of the lemma. We could have obtained it from the first form by applying the operation we have called flip; but we prefer to derive flip from the two forms of the Case Analysis Lemma, as follows. Let E = ( (ab) ((a)c) ); then Ea = b Applying the Lemma, we get: E = ( (ab) ((a)c) ) - back where we started, so no progress there. However, applying the second (alternative) form of the Lemma: E = (a(b)) ((a)(c)), and thus flip is proved. In fact the Case Analysis Lemma, powerful though it is, lies just a few steps away from the axiomatic foundations of the CL-calculus (i.e. the initial equations). It depends only on copy (to any depth) and each way; and each way depends only on complements and distribute: e = e ((x)((x))) [complements] It will be no bad thing to re-derive each way from the initial equations, to remind ourselves of the shortness of the path connecting them. We have: e = e(()) = e(()x) = e((x)x) = e((x)((x))) = e ((ex)(e(x))) The nested brackets are tiresome to read: much better get out your pen and paper and draw out the steps properly. Alternatively, re-enact the sequence of steps in the Play Area:
Here is the sequence leading to the alternative form of each way (step through the sequence by clicking on the arrows; the first move is to wrap e):
Exercise for the reader [April 2016]: I can now get from e to (x(e)) ((x)(e)) in just six elementary steps. (Each step one of (un)wrap, (un)delete or (un)copy.) See if you can do the same. One may use the Case Analysis Lemma simply as a tool for simplifying expressions. For Ex and E(x) each involve one fewer letter than E did (namely, they do not contain the letter x); and are therefore already simpler than E in that respect. A simple example: let E = ( a (br) (cr) (dr) (er)). Then Er = ( a (b) (c) (d) (e) ) Then the second form of the Lemma gives us E = (r(Er)) ((r)(E(r))) This is a derivation of the equation we called modified distribute. Another example of the fruitful use of the Lemma for simplification is to be found on this page: Lewis Carroll's Five Liar Problem. Notes[1] This is essentially Theorem 15, 'Canon with respect to a variable', of Laws of Form (1st edition, page 41). The proof there, especially when expanded from the rather condensed form given in the book, is considerably more complex than the one given here. (See this page, from an earlier version of this web-site, for an expanded version of the original argument.) back to Proof by Mutual Dominance |