Suppose the nodes of the tree of partial valuation strings are initially coloured white. Suppose further that we then we traverse the tree of partial valuation strings, one level at a time, colouring each 'marked' node red, leaving the rest white. Note that it is a finite operation to determine whether a node is marked by the generative expression, as only a finite number of ground instances have to be tried out. (That was the point of insisting that the ground instance that does the marking must have level n or less.) We make the following important observation:
any descendant of a red node is red.
For, the ground instance that marked the shorter partial valuation string (corresponding to the ancestor node) will also mark the longer partial valuation string (corresponding to the descendant node). Therefore, by a variant of 'logical transposition',
any ancestor of a white node is white;
and the set of white nodes, linked by the same lines of descent as in the original tree, itself constitutes a rooted tree - no longer, indeed, a binary tree, but a tree in which each node has 0, 1 or 2 descendants.
The tree that consists of all the white nodes may be thought of as the result of pruning the original tree, by cutting off all the red (marked) nodes. Each time a red node is cut off, all its descendants are cut off as well. This is as it should be - and saves a certain amount of the labour of pruning the tree!
An exceptional case is when the root node, corresponding to the partial valuation string of zero length (i.e. the void) is marked by the generative expression; this implies that the expression has a ground instance of level 0, that is, a ground instance containing no ground atoms. Since a ground substitution can only change an atom, never make it go away, it must be the case that the expression contains no atoms at all (not even atoms of arity zero), and so must be a C-expression. Furthermore, if it is to mark the partial valuation string of length zero, the C-expression must be mark-equivalent. In this case the pruning gets rid of the whole tree.
If we allow ourselves the Law of the Excluded Middle, we may say:
either the pruned tree is finite, or it is infinite
(that is to say, there is no middle condition between finite and infinite). Let us consider the second case first, and make use of another idealist (or non-constructive) principle, namely König's Lemma. This says that any infinite, finitely generated tree must have an infinite branch. Finitely generated means that no node has more than a finite number of children, a condition we meet easily in our tree, as every node has at most 2 descendants. The proof (adapted to the case in hand) is easy. Let us call a node 'good' if it has infinitely many descendants. The root node is definitely good (else the whole tree would be finite, contradicting our premise). Moreover, each good node must have a child that is good (else the parent node would not be good after all). Therefore, starting at the root node, we may climb to any level in the tree, stepping only on good nodes. Because of the goodness of each node that we stand on, our path upwards through the tree cannot end: it is therefore what we call an infinite branch. (Note the non-constructive element here: how can we actually tell whether or not a child-node is good, except by completing an unbounded number of node-tests? The mathematical idealist says, Never mind how you find which one it is, it is enough that you know that one of them must be good!)
Translating back into the language of partial valuation strings, if the pruned tree is infinite (implying that it is infinitely high) there is a complete white valuation string, i.e. a complete valuation string which is unmarked by any ground instance of the expression. To put it another way, there is a complete valuation string which reduces every ground instance of E to _ .
So much for infinite pruned trees. We now draw out the consequences of the pruned tree being finite. In this case the pruned tree has a node of highest level, above which there are no more nodes. Returning to the original tree (before pruning), where each node was red or white, we can say that the first level above the highest white node – level m, say – consists entirely of red nodes. Each of the corresponding partial valuation strings is marked by a ground instance of E: Eθi, say, with i running from 1 to M=2m, so that there is a θi corresponding to each partial valuation string of length m. Now consider the expression
Eθ1 Eθ2 Eθ3 ... EθM.
This will be reduced to the mark by any of the partial valuation strings of length m. Therefore, by Theorem 2.6(b),
Eθ1 Eθ2 Eθ3 ... EθM = O .
Therefore, by Lemma 2.11, E is mark-equivalent. In summary, we have demonstrated the following:
Given any CLS-expression E, one of the following statements is true, the other false: 1) E has a complete 'white' valuation string 2) E ≅ O. Here 'white', we may recall, means that the valuation string reduces every ground instance of E to _ (so the string is 'unmarked' by E).
Using the fact that valuation strings are not affected by substitutions, we may state the theorem in the following alternative form:
Given any CLS-expression E,
E ≅ O iff for all complete valuation strings V, V E ≅ O .
Suppose E ≅ O ; then, since statement 2) of theorem 2.14 is true, statement 1) must be false; therefore, given any V there is a ground instance Eθ of E that is contradicted by V, in other words
V Eθ = O
V E [1+θ] = O
V E ≅ O .
Conversely, suppose that for all V, VE ≅ O. Then by Lemma 2.11, for each V there exists a set of substitutions θ1 .. θn such that
O = [VE]θ1 [VE]θ2 ... [VE]θ2
∴ O = V Eθ1 Eθ2 ... Eθn
(because V, being 'ground', is not affected by any substitution). Now, by Lemma 2.8, we may subject each side of this equation to any substitution φ and the equation will still be valid. Choose for φ a substitution which eliminates all remaining mutables from the right- hand side, and turns each instance of E there into a ground instance:
O = V Eθ1φ Eθ2φ ... Eθnφ.
Now V, being a complete valuation string, has the power to the reduce all these ground instances to C-expressions, that is, to _ or O . The equation says that one of them, at least, must be reduced to O. Thus
V Eθiφ = O ,
for some i, implying that V is marked by this particular ground instance of E. But this argument applies to all complete valuations, therefore no complete valuation string is unmarked, and statement 1) of theorem 2.13 is false; therefore statement 2) is true and E ≅ O ◊
Theorem 2.15 gives us our final criterion for the mark-equivalence of a CLS-expression E. It may be thought of as the equivalent, in CLS, of the CL-theorem Theorem 2.6(b).