CHAPTER EIGHT

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 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:

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 ≈ 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:

Lemma 8.2

If W_sk is satisifable then E has a complete white valuation string.

Proof

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₁, G₂, G₃, G₄, ...}; then a complete valuation string is an expression of the form

V = H₁ H₂ H₃ H₄ ...

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 ◊

---

Lemma 8.3

Suppose E has a complete white valuation string V. Then W_sk = Π_xΠ_x...Π_z E is satisfiable.

Proof

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 ◊

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

Proof

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.

Proof

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 P₁, P₂, ... 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₁∧P₂∧ ... ∧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:

Example 8.7

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.

---