## Development of the Equivalence ExpressionWe define [A|B] = (A(B))((A)B) . There is an equivalent 'flipped' form: [A|B] = ( (AB) ((A)(B)) ). The following properties follow easily from the definition: [A|B] = [B|A] The last of these is a little harder to prove: [A|C] = [A|[A|B]] = (A([A|B]))((A)[A|B]) Now for the most
[A|B] A = [A|B] B
[A|B] A = [ |B] A [uncopy] (Alternatively, refer to the direct proof of Lemma 8 in Proof by Mutual Dominance.) Thus, [A|B] (...((AP)Q)R...)V = [A|B] (...(([A|B]AP)Q)R...)V One may think of [A|B] as ## NestingConsider the expression E = [A | [B|C] ]. Certainly, the interchange of B and C makes no difference to E; what is not so obvious is that neither does the interchange of A and B. So [B | [A|C] ] = E. One way to see this is to expand the square brackets into circle-letter expressions. Thus [B|C] = (B(C))((B)C) = ((BC)((B)(C))) a form which is clearly insensitive to any permutation of A, B and C. Let's call this 'triadic symmetry'. Now let's go up a level and consider F = [A|[B|[C|D]]] . Applying triadic symmetry to B, C, D we see that F is insensitive to any permutation of B, C, D. Applying it to A, B, [C|D] we see that [B|[A|[C|D]]] = F . Now A, C, D may be permuted at will; then C or D may be got into the outer position, and the other letters permuted at will. So F is insensitive to all permutations of A, B, C and D. But more is true. Again applying triadic symmetry to A, B and [C|D] we may get [C|D] into the outer position, so F = [ [C|D] | [A|B] ] . So the square brackets may be It's time for a theorem. Let Q = [a|[b|[c|...[j|k]...]]] be denoted 'the equivalence expression of the N letters a,b,c... up to k'. Then Q is equivalent to any other expression Q' formed out of the N letters and the N-1 pairs of square brackets, no matter what order the letters are taken in, and no matter how the forms [|] are nested. (We just assume that each compartment of each form [ | ] is occupied either by a letter or by another bracket-form.) Even when N=5 you can see that there will be quite a few permissible nesting schemes - and the situation will only get worse as N gets larger.
Now suppose that just one of the substitutions changes, so O is substituted for one of the letters rather than _ . At the place in Q where that letter occurs, [_|_] will change into [O|_] = O. Then the change will propagate up to the next level, and then to the level above that, all the way to the top. Therefore Q will change its value from _ to O. Now suppose that we substitute O instead of _ for a second letter. Again this will We may imagine changing the substitutions again and again, always just one letter at a time. Then each change will result in Q changing its value. Therefore, after an odd number of changes, the value of Q will be O; after an even number of changes, it will be _ . In other words, Q will have the value O if the number of marks O among the letter-substitutions is odd, but the value _ if the number is even. Let Q' be another equivalence expression, involving the same letters, but with the letters permuted, and with the brackets differently nested. Again, when _ is substituted for all the letters, Q' will take the value _ . Again, when any single substitution is changed, the value of Q' will change. Therefore, Q' and Q will always have the same value, no matter what values are substituted for the letters. Therefore, by the Case Analysis Theorem, Q' and Q are equivalent expressions in the CL-calculus. We use the following form to denote the multiple equivalence expression of the letters a, b, .. up to k: [a|b|... |k] When we are working graphically we use the form It makes no difference if the letters are put into their compartments in a different order; and the expression is equivalent to any nested form such as:
Q = [x|a|b|...|f] , any occurrence of x, at any depth, may be replaced by [a|b|...|f].
[x|[a|b|...|f]] , so the usual application theorem may be applied.
[x|a|b|...|f] [x|m|n|...|q] = [x|a|b|...|f] [a|b|...|f|m|n|...|q] .
[x|y|a|b|...|f] [x|y|m|n|...|q] = [x|y|a|b|...|f] [y|a|b|...|f|y|m|n|...|q] because [y|y] = _ . For an example of the use of multiple equivalence expressions, see the page on Lewis Carroll's Five Liars Problem. back to The Mutual Dominance Lemma |