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

hence

hence

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:

hence

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

Transcription of ¬C:

hence

hence

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.

##### Solution

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

• • is associative: ∀x,y,z (x•y)•z= x•(y•z)
• every x satisfies e•x = x•e = x
• each x has an inverse y such that x•y = y•x = e

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.