Examples (Part Two)

Example 10.7

(From Quine, quoted by Smullyan p 57 - described as difficult...)

P1 (∀x ((Fx ∧ Gx) → Hx)) → (∃y (Fy ∧ ¬Gy))
P2 (∀u (Fu → Gu)) ∨ (∀v (Fv → Hv))
C (∀s ((Fs ∧ Hs) → Gs)) → (∃t (Ft ∧ Gt ∧ ¬Ht))

Transcription of P1:



We note that P1 is not yet actually in clausal form; however, it proves more convenient, on this occasion, to keep it as it is. The transcription of P2 is:


Πu and Πv can migrate to the outer space (up two levels), and can then be discarded, leading to

Transcription of ¬C:



The combined expression P1∧P2∧¬C then resolves as:

We note that the 'resolution' between the second and third clauses involves first the substitution {x/t}, then an application of the CL-rule

A (A(B)) = AB ≥ B

(where A and B are any CL-expressions), and is therefore perfectly admissible in a proof of the claim that a CLS-expression is mark-equivalent - which is what we are doing here.

If desired, the proof can be done 'by the book' - i.e. using clausal resolution. The first thing is to convert the premise P1 into clausal form, which can be done by using the CL-rule

repeatedly. Thus P1 is transformed as follows:

Now combine with

(Ft Gt (Ht))

and 'breed'. It is left as an exercise for the reader to obtain the clauses Fy and (Gy) by this means. (Answer here.)

Example 10.8

(From Robinson's 1963 paper, 'Theorem-proving on the computer', J. ACM 10 (Apr 1963), 163-174.) This is an example where we get serious about unification!

This example is taken from the field of Abstract Algebra. Suppose A is an algebra with a binary operation •. Thus, given any two elements x and y, they may be combined using • to produce a third element z; a situation which we symbolize by the equation

x•y = z.

Suppose further that • has the associative property, that is, for any three elements x, y and z,

(x•y)•z = x•(y•z);

and also, given two elements x and y, there are elements a and b satisfying the following equations:

a•x = y
x•b = y .

Show that the algebra has a left-inverse: that is, an element e such that

e•x = x

holds for every element x.


We first symbolize the known facts about A, and the statement that is to be proved, by formulae of first order logic.

The existence of • we represent as follows:

P1 ∀x ∀y ∃z Qxyz

Here the predication Qxyz means 'z is the result of combining x and y using •'. One way of representing the property of associativity would be to introduce a second two-place predicate meaning 'equals'; but there is another way of doing it. We make the statement:

P2 ∀x ∀y ∀z ∀u ∀v ∀w (Qxyu∧Qyzv) → (Qxvw ↔ Quzw)

In words: if u is x•y, and v is y•z, then w is x•v iff w is u•z. The remaining premises are:

P3 ∀x ∀y ∃a Qaxy
P4 ∀x ∀y ∃b Qxby

The statement to be proved is

C ∃e ∀x Qexx

When we transcribe into Laws of Form notation, P2 (associativity) may be split into two clauses:

P1, P3, P4 and ¬C become simply

For the proof by resolution, we need only the first clause of P2, and do not need P1; we also use P4 twice. The resolution-scheme is:

(click on the diagram to bring up a magnified version). This is heavily dependent on unification - perhaps a more detailed explanation is in order? The first resolution step involves unification (one-making) of the terms

Qxvw, Qexexe .

This is achieved by the substitution

{ e/x , xe/v , xe/w } .

Remember, the substitution acts on the whole of both expressions which are participating in the resolution step, so all occurrences of x, v and w are replaced by the specified terms. The second step involves unification of

Qeyu, Qakmkm,

achieved by means of

{ y/k , u/m , ayu/e }.

This is why the term xayu appears in the resolution product. Next, we unite

Quzxayu, Qnbnpp

by means of

{ u/n , xayu/p , buxayu/z };

and finally we must unite

Qybuxayuxayu, Qibijj.

Acting on the two terms at first with the substitution { y/i , xayu/j }

they become

Qybuxayuxayu, Qybyxayuxayu.

All that is needed to achieve complete union is to follow up with the substitution

{ y/u }

(or vice versa); then the term in the circle can be uncopied, leaving the sought-for empty mark - our goal! It is interesting that the 'automatic' resolution process finally arrives at the 'insight' that y must be set equal to u - even though it leaves it to the last possible moment. Whereas a typical human approach to the problem of deriving our conclusion C starts with the insight that if there is a left-identity e, then it must coincide with a solution of the equation

ex = x, ...(1)

where x is some arbitrarily chosen element of A. (The equation must have a solution by premise P3.) A 'human-style' proof might continue as follows:

Let c be any element of A; then, by P4, there exists a element b such that

x•b = c . ...(2)

Then e•c = e•(x•b) (by (2))
= (ex)•b (by P2)
= x•b (by(1))
= c (by(2)).

But c was any element of A; we may therefore conclude:

∀c e•c = c,

a statement which verifies our original claim C ◊

Let's see how our 'human' proof could be formalized in the language of the CLS-calculus. Let x be a fixed element of A. We first note that

Qaijij » Qaxxxx

(the left-hand expression reprents the premise P3). Secondly, flowing from P4

Qfbfgg » Qxbxcc

Next, bringing in the first clause of P2, and repeating the consequence of P4 just derived:

Qaxxxx Qxbxcc Qxbxdd (Qxyu Qyzv Quzw (Qxvw))
» Qxbxdd (Qxbxcw (Qaxxcw))
» Qaxxdd

Thus our conclusion is 'implicated' in the premises. The skill lies in revealing that fact; it could be compared with the skill of the sculptor, who reveals the figure that is 'implicated' in the block of marble.

Example 10.9

Our final example on this page is another example used by Robinson, again from the field of Abstract Algebra. The problem is this. Let G be a group, with binary operation •, identity element e, and in which every element x satisfies the equation

x•x = e

(so every element has order two). Prove that G is commutative, i.e. for every pair of elements a, b

a•b = b•a .

To tackle this, we first need to recall the group axioms. A group is a set G with • and e such that

In this problem, the third axiom is redundant, as each element is its own inverse. This leaves us with five premises and a conclusion, as follows (P1 and P2 are the two halves of the statement of associativity, as in Example 10.8):

P1 ∀x ∀y ∀z ∀u ∀v ∀w (Rxyu∧Ryzv∧Ruzw) → Rxvw
P2 ∀x ∀y ∀z ∀u ∀v ∀w (Rxyu∧Ryzv∧Rxvw) → Ruzw
P3 ∀x Rxxe
P4 ∀x Rexx
P5 ∀x Rxex
C ∀a ∀b ∀c Rabc → Rbac
¬C ∃a ∃b ∃c Rabc ∧ ¬Rbac

For the proof by resolution, we proceed in four stages:

Stage 1

We use P1, P3 and P5:

(The grey arrows indicate the terms that are united at each step. L1 is used as a label for the second resolution product, as is L2 in the next stage.)

Stage 2

We use P2, P3 and P4:

Stage 3

This time we use the first half of ¬C, L1 (twice), and L2. Note that when L1 is applied to a term Rxyz it has the effect of swapping the 1st and 3rd indices; L2 on the other hand swaps the 2nd and 3rd indices.

Stage 4

We bring in the second half of ¬C:

It is left as an exercise for the reader to translate the resolution-proof into a human-friendly form.