We saw in the last chapter that any wff W of predicate logic has a Skolemized version
W_{sk} of the form

W_{sk} = Π_{x}Π_{x}...Π_{z} E

where E is a Pi-free formula made of circles and 'atomic formulae' (consisting of predicate-functions with subscripts; the indices, or elements of the subscripts may be subscripted in turn if they are 'constants' rather than variables). It will not have escaped the reader that such a formula has precisely the form of what we earlier called a CLS-expression. (That was in Chapter 1; CLS stands for Circle, Letter and Subscript.)

Thus to each wff we may associate a CLS-expression. We will refer to the process that leads from wff to CLS-expression as 'transcription', and say that E, in the above example, is the CLS-transcript (or just 'transcript') of W.

Chapter 2 instituted a Great Divide among CLS-expressions. As detailed in the 'Dichotomy Theorem', 2.14, there are those CLS-expressions which are mark-equivalent; and there are those which have 'complete white valuation strings' - and ne'er the twain shall meet! Each expression falls into one or the other category. (We'll have a little recap on what all this means in a moment.) When E is the CLS-transcript of a wff W, does the category of E (i.e. whether it is mark-equivalent, or has a complete white valuation string) have any significance for W? It turns out that it does: we will prove the following theorem:

Let W be a wff, E its CLS-transcript. Then W is satisfiable if and only if E has a complete white valuation string.

Because W ≈ W_{sk} (they are equal as regards satisfiability), what is claimed
by the theorem is that W_{sk} is satisfiable iff E has a complete white valuation
string. In fact, we'll treat each half of this restatement as a Lemma and prove them separately:

If W_{sk} is satisifable then E has a complete white valuation string.

Like all CLS expressions, E has its very own Herbrand Universe (or set of ground terms), a set of ground atoms, and a set of ground instances, all of which are either finite or countably infinite. (Refer back to Chapter 2 for the definitions: the main idea is that anything is described as 'ground' if all mutables have been eliminated from it, in favour of immutables.)

Suppose the set of ground atoms is {G_{1}, G_{2}, G_{3}, G_{4}, ...}; then a complete
valuation string is an expression of the form

V = H_{1} H_{2} H_{3} H_{4} ...

in which each H_{i} is either G_{i} or (G_{i}). Any complete valuation string
such as V has the following property:
when put next to a ground instance of E, such as Eθ, the whole expression is CL-equivalent either to V, or to the mark.
We say that 'V has the power to reduce Eθ to _ or O'. This is because Eθ is an expression consisting of
circles and ground atoms; each ground atom can be removed ('uncopied'), in the presence of V, and replaced either by _
or by O.

V is described as 'white' if it reduces every ground instance of E to _ .

Let us recall what it means for W_{sk} to be satisfiable.
It means that W_{sk} has a model M such that its value in M is _ . So there is
a universe of discourse, U; and
each constant appearing in W_{sk} is assigned a U-element, to which it refers. In case of a subscripted constant,
each one of its instantiations (resulting from replacement of variables appearing in the subscript,
by U-elements) must be assigned a U-element. Furthermore, every instantiation of an
atomic formula occurring in W_{sk}
is given a value. (This is what we call 'giving the facts'.)
In other words, every atomic formula, all of whose arguments are constants or subscripted constants,
with no non-constants occurring in the subscripts (i.e. what from the CLS point-of-view one would call a "ground atom")
has a value, _ or O.

This allows us to build up a complete valuation string for E, based on M. Let's call it V. If an instantiated
atomic formula,
having the appearance of a ground atom,
G_{i} say,
has the value _ in M then we include G_{i} as it is in V. If the value is O then we include (G_{i})
in V, instead. In this way we can go through all the ground atoms, adding them to the valuation
string, either *au naturel* or dressed in a circle.

We claim that V so defined is 'white'. For consider any ground instance Eθ of E. This consists
of a pattern of circles sprinkled
with a number of ground atoms. On the one hand, considered as a formula of predicate logic this expression has a value in M.
This value is determined by the values of the ground atoms: when the values are substituted for the
ground atoms the formula becomes a C-expression which reduces to _ or O.
The fact that M *satisfies* W_{sk} implies that the ground-atom-values are so disposed that, in fact, the C-expression
always reduces to _ . However, this substitution of ground-atom-values can be mimicked by placing V next to Eθ, then
uncopying all the ground atoms out of Eθ. Given that replacement-by-value produces a void-equivalent expression,
so does the uncopying, therefore

V Eθ = V .

But this is the case for all ground substitutions θ; therefore, V is white ◊

Suppose E has a complete white valuation string V. Then W_{sk} =
Π_{x}Π_{x}...Π_{z} E is satisfiable.

We proceed by constructing a model M which satisfies W_{sk}. First,
M needs a universe of discourse. For this we
choose the Herbrand universe of E. (At last we understand why it is called a 'universe'!) This seems a bit peculiar,
but it turns out to be OK, as we shall see. The universe of discourse, U, just has to be a set of somethings:
so why not a set of ground terms?
(In particular: the set consisting of *all* the ground terms that can be generated by the constants and subscripted
constants occurring in E.)

In addition to its universe, a model for W_{sk} needs a) references for all constants that occur in
W_{sk}, and for
all instances of subscripted
constants that occur in W_{sk} and b) 'the facts'. Now, instances of a subscripted constant are obtained by
substituting U-elements for all the variables occurring in the subscript. But in this case, a U-element
is simply a ground term; therefore an *instance* of a subscripted constant is always just another ground term.
(As is an unsubscripted constant.)
There is only one sane way of specifying the U-element that a ground term refers to: it must refer to itself!
At any rate, that will be our choice.

What about 'the facts'? It will be recalled that what we mean by this is that every instantiation of an atomic
formula is given a value. In this case, an instantiation of an atomic formula is none other than a ground term: so a
value must be ascribed to every ground term. But this is just what V does for us. Suppose we say that V itself must
have the value _ in M; then all the ground atoms that appear uncircled in V must have the value _ , all the circled
ones, O. The fact that V is white implies that all instantiations of E have the value _ , therefore W_{sk} itself
has the same value. We have a model that satisfies W_{sk} ◊

Theorem 8.1 follows from Lemmas 8.2 and 8.3 ◊

By logical transposition: W is unsatisfiable if and only if E has no complete white valuation string ◊

W = O (W has the value False in all models) if and only if E≅O

W = O (in all models) says the same as 'there is no model in which W =_{M} _ ' in other words W
is unsatisfiable. The statements, 'E has no complete
white valuation string' and 'E≅O', imply each other by
by Theorem 2.15. Therefore Theorem 8.5 follows from Corollary 8.4 ◊

A necessary and sufficient condition for W=O is the following: if E (derived from W by Skolemization and removal of Pi's) is put into clausal form and subjected to the resolution breeding process, the process generates the mark O after a finite number of generations.

This follows from Theorem 8.5 together with Theorem 4.12 (Resolution Theorem) ◊

Suppose we have a notion that a certain statement C (for conclusion) is implicated in a set of premises
P_{1}, P_{2}, ... P_{k}. We let the same letters stand for the well-formed formulae
representing the statements. The implication is valid if and only if the statement

W = P_{1}∧P_{2}∧ ... ∧P_{k}∧¬C

is unsatisfiable - i.e. there is no model in which all of the P_{i} are true but C is false.

Thanks to Corollary 8.6 we know how to test the unsatisfiablity of W: Skolemize, remove Pi's, put into clausal form, breed. If the mark is produced in a finite number of generations, fine, we're done, the implication is good.

But what if we keep turning the handle and the mark never quite comes? In that case we are left in radical uncertainty: we simply don't know if the mark might appear eventually, or if on the contrary it never ever will - which would be the case if our implication was after all invalid.

In fact there are two ways in which the mark could never appear. Either the breeding process could stop producing anything new; or it could carry on forever producing new clauses - but never the empty clause, the one we are after. A simple example of the latter state of affairs is as follows:

Suppose W is the conjunction of the two statements

∃z Nz

∀x ( Nx → (∃y Ny Sxy) )

and suppose I have got it into my head that W is unsatisfiable, and want to put it to the test. My first step is to transcribe W into Laws of Form notation:

then to get rid of ∀, ∃ in favour of Π:

Next, Skolemize and drop the exterior Pi:

This is not yet in clausal form; by a CL operation we get to

Let us call this expression F. The next step is to breed from the three clauses of F (using unification and resolution), and see if we can obtain the mark by this means. (If we can, then W is unsatisfiable, as we suspected.)

The first two clauses are kindred - just substitute **z** for x. Their resolution product is

N**y**_{z}

But this is again kindred with the second clause of F and will resolve with it to produce

N**y**_{yz}

and so on. Thus we obtain an endless succession of resolution products - but getting no closer to O... We also get the following by resolving with the third clause:

S**zy _{z}**, S

In fact it is clear that W is *satisfiable*. If for our model we take the natural numbers {1, 2, 3, ...}, with
**z** referring to 1, Val[Nx]=_ for all x, and Val[Sxy]=_ iff y is the successor of x; then Val[W]=_. So this is
an example where the breeding process never stops, but where we can be sure that O will never be produced ◊

We see that our criterion while undoubtedly sound, and even quite efficient in certain cases,
does not quite provide a means to *decide* whether or not an
implication is valid. We here use 'decide' in a somewhat technical sense, roughly, to determine by finite
algorithmic means. Our criterion has the great virtue of being algorithmic; but it fails to be decisive
as the algorithm is not guaranteed to terminate.

Might there exist a superior algorithm, testing for mark-equivalence but guaranteed to terminate? On the basis of our acquaintance with the Resolution Method, the existence of a superior algorithm does not seem particularly likely. There would have to be something 'magic' about it. In fact the possibility is ruled out by the Undecidability Theorems proved by Church and Turing in 1936 and 1937 respectively.