The Bridge

from First Order Logic to the CLS-Calculus

We saw in the last chapter that any wff W of predicate logic has a Skolemized version Wsk of the form

Wsk = Π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:

Theorem 8.1

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 ≈ Wsk (they are equal as regards satisfiability), what is claimed by the theorem is that Wsk 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:

Lemma 8.2

If Wsk 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 {G1, G2, G3, G4, ...}; then a complete valuation string is an expression of the form

V = H1 H2 H3 H4 ...

in which each Hi is either Gi or (Gi). 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 Wsk to be satisfiable. It means that Wsk has a model M such that its value in M is _ . So there is a universe of discourse, U; and each constant appearing in Wsk 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 Wsk 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, Gi say, has the value _ in M then we include Gi as it is in V. If the value is O then we include (Gi) 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 Wsk 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 ◊

Lemma 8.3

Suppose E has a complete white valuation string V. Then Wsk = ΠxΠx...Πz E is satisfiable.


We proceed by constructing a model M which satisfies Wsk. 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 Wsk needs a) references for all constants that occur in Wsk, and for all instances of subscripted constants that occur in Wsk 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 Wsk itself has the same value. We have a model that satisfies Wsk

Theorem 8.1 follows from Lemmas 8.2 and 8.3 ◊

Corollary 8.4

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

Theorem 8.5

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 ◊

Corollary 8.6

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) ◊

Testing Implications in Predicate Logic

Suppose we have a notion that a certain statement C (for conclusion) is implicated in a set of premises P1, P2, ... Pk. 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 = P1∧P2∧ ... ∧Pk∧¬C

is unsatisfiable - i.e. there is no model in which all of the Pi 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:

Example 8.7

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


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


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:

Szyz, Syzyyz, ...

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.