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.