Development of the Equivalence Expression
[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 useful property of [A|B]:
[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, in the presence of [A|B], A may be changed into B, and vice versa, at will. Moreover, A may be changed into B even if A is buried within an expression E, just so long as E is 'in the presence of' [A|B]. This is thanks to the fact that [A|B] may then be copied into the space in which A resides, may do its work of transforming A into B, and may then be uncopied again. So
[A|B] (...((AP)Q)R...)V = [A|B] (...(([A|B]AP)Q)R...)V
One may think of [A|B] as catalysing the conversion of A into B. It must be present, but is not itself transformed by the transformation.
Consider 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 nested in a different way, and it still makes no difference to F.
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.
Proof: we make use of 'Exhaustive Case Analysis'. To this end we must consider the value of Q when arithmetic values ( _ or O) are substituted for all of its letters. Suppose we start by substituting _ for every letter. Wherever [ | ] occurs in the resulting expression, we may replace it by _ . Eventually, all the brackets will disappear and in no time at all Q will be reduced to _ .
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 change the value of the square bracket expression in which the letter occurs - whether the change is from _ to O or from O to _ . And the same will happen to all the 'higher up' brackets containing that first one, all the way up to the top. So once again Q will change its value - from O to _ .
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:
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:
Lemma: in the presence of
Q = [x|a|b|...|f] ,
any occurrence of x, at any depth, may be replaced by [a|b|...|f].
Proof: Q is equivalent to
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
on to The 'Case Analysis' Lemma