For our final, extended - not to say rambling - example we return to Group Theory, this time to
the very beginnings of the theory -
the axioms. It is normally said of the identity element **e** that both **e**•x and x•**e**
must equal x for all elements x; similarly, it is said of the inverse x^{-1} of x that both x^{-1}•x
and x•x^{-1}
must equal **e**. However, it is in fact sufficient to posit just the first of each of these
pairs of statements, that is, that **e** is a 'left identity element' and that x^{-1} is a 'left inverse'
of x. The other properties ('right identity element' and 'right inverse') follow from the first ones.

We would like to be able to show, then, that associativity, left-identity and left-inverse together imply
right-identity and right-inverse. To start with we will focus our attention on just the first
conclusion (right-identity). To make it a bit more formal, we would like to show that C follows from
P_{1}, P_{2}, P_{3}, P_{4}, where the
statements are defined as follows:

P_{1} |
∀x ∀y ∀z ∀u ∀v ∀w (Rxyu∧Ryzv∧Ruzw) → Rxvw |

P_{2} |
∀x ∀y ∀z ∀u ∀v ∀w (Rxyu∧Ryzv∧Rxvw) → Ruzw |

P_{3} |
∀x Rexx |

P_{4} |
∀x ∃y Ryxe |

C | ∀x Rxex |

¬C | ∃x ¬Rxex |

Converting into CLS-expressions, our task is to show that the following expression is mark-equivalent:

You may like to try your hand at a direct approach to this problem, 'breeding' new expressions by resolution. I think you will soon find that the number of possible combinations is so great that progress toward the goal (the mark) is impossible. I decided to aim much lower, and see if I could adapt an existing (well-known) demonstration of the theorem to the CLS method. Even this turned out to be not without its own difficulties, as we shall see. Let's start by looking at the existing proof of the theorem that 'right-identity' follows from associativity, left-identity and left-inverse. It begins by establishing a lemma:

**Lemma** If h•h = h then h = **e**.

**Proof** Let g be the left-inverse of h, so g•h = **e**. Then

**e** = g•h = g•(h•h) = (g•h)•h = **e**•h = h ◊

Getting back to the main proof, let x be any element of G, and let y be its left-inverse; and let

h = x•y.

Then

h•h = (x•y)•(x•y) = ((x•y)•x)•y = (x•(y•x))•y =
(x•**e**)•y = x•(**e**•y) = x•y = h.

Therefore, applying the lemma,

x•y = h = **e**,

and

x•e = x•(y•x) = (x•y)•x = **e**•x = x Q.E.D.

It will be noted that the proof requires no less than five applications of associativity (i.e. P_{1} and/or
P_{2}), as well as numerous applications of each of P_{3} and P_{4}. In addition
it makes much use of the notion of *equality* between group elements. But equality is not explicitly
mentioned in our premises; at most implicitly in the use of the 3-place predicate Rxyz, which makes the claim that
the combination of x and y (i.e. x•y) *equals* z.

To explain the problem with equality, let's think what is involved in translating the lemma into
CLS-language. The immediate problem is that the conclusion of the lemma 'x = **e**' *cannot be expressed*
in terms of the predicate Rxyz. Even to express the conclusion there is nothing for it but to
introduce a new 2-place predicate Exy with the meaning 'x equals y'.

The core of the proof of the lemma is the fact that the triple product

**i**_{h}•h•h

can be construed in 2 different ways

(**i**_{h}•h)•h and **i**_{h}•(h•h),

equivalent to

**e**•h and **i**_{h}•h,

respectively, by P_{4} and by hypothesis (h•h = h). These combinations are equivalent,
in turn, to h and **e**, respectively. But P_{1} and P_{2} won't quite yield us this result.
Rather, they yield us the results

**i**_{h}•h = h and **e**•h = **e**,

respectively.
Of these, the second statement looks most promising; for, put together with P_{3}, which implies
**e**•h = h, it would seem to imply

E**e**h,

i.e. that **e** and h are equal. However, 'seems to imply' is really not good enough - we are trying to
do logic, after all! To do this thing properly, we need to define the properties of the relation (i.e.
2-place predicate) Exy. It looks like one of these properties ought to be:

In words: if it is the case, for some x, y, a and b that the combination of x and y is a,
and also that the same combination is b,
then a equals b. That seems reasonable enough - or self-evident, as axioms are supposed to be - doesn't it?
Besides, it
gives us what we want, which is that h 'equals' **e**. We are now in a position to state and prove the lemma
in the language of CLS. Just before that, I am going to slip in a little change. We don't want our hypothesis
(translating h•h = h) to be Rhhh because, by the usual rules of interpretation, this would mean that
Rhhh is true *for all* h. Rather, our hypothesis is that there is one particular h satisfying
h•h = h; we express this by changing h into an immutable **h**. Here then is our lemma:

(For the meaning of the symbol » refer back to Chapter One.)

We first resolve P_{2} with R**hhh** and two copies of P_{4}. There is clearly a certain
amount of choice as to which terms we attempt to unite (as R... and E.. are the only predicate-functions in town).
Let us be guided by the 'natural language proof' of the lemma. Recall that this was based on the triple product
**i**_{h}•h•h; this tells us that i_{h} will match up with the mutable
x in P_{2}, **h** with y and **h** with z. So the term R**hhh** will match up with,
indeed, unite with the term Ryzv within P_{2}. Let's do that resolution first:

(the unifying substitution is simply {**h**/y, **h**/z, **h**/v}.) To unite the two remaining terms
at level -1 with 2 copies of P_{4} the unifier is {**h**/q, **h**/r, **i _{h}**/x,

Note that we haven't bothered to draw in the intermediate resolution-product. In fact all three resolution-steps
so far employed can be viewed as a single *compound* resolution step resulting from the union of the compound terms

Rxyu Ryzv Rxvw, R**i**_{q}q**e** R**hhh** R**i**_{r}r**e**

The unifier is the combination of the substitutions already given; and once the compound terms are united, the copy
inside the circle can be uncopied (all three sub-terms at once), giving the result R**ehe**. We may use the following
terminology to represent the whole process:

Res(P_{4}, R**hhh**, P_{4}, P_{2}) = R**ehe** .

Now that we have obtained the term R**ehe** we only need to resolve it with P_{3} and the
equality premise E_{1} to complete the proof of the lemma:

Q.E.D.

(We have obtained the statement E_{eh}. What we can actually *do* with it is another question,
which we will address in due course.)

Actually, for our main proof we will need a lemma that is slightly stronger than the one just proved. The one we have
only works for one particular **h**; ideally, we want one that works for *any* h that just happens
to satisfy h•h = h. We obtain the slightly stronger lemma simply by omitting the premise
R_{hhh} and seeing what we are given by the resolution process. This is the result:

P_{4}P_{2}P_{3}E_{1} » (Raba (E**e**b)).

We resolve P_{2} with two copies of P_{4} by uniting the compound terms

Rxyu Rxvw, R**i**_{p}p**e** R**i**_{q}q**e** .

The unifying substitution is determined as follows:

x =i_{p}=i_{q}∴ q = p y = p u =ev = q = p w =e

Therefore Ruzw = R**e**z**e**, and the resolution product is

Now resolve this expression with P_{3} and E_{1}:

and the lemma is proved ◊

The original lemma may be obtained from the stronger one by adding R**hhh**
into the premises and resolving◊

Now we've got the lemma out of the way, we return to the main proof, which starts

'Let h = x•**i**_{x}'

How do we translate this? We can't just posit Rx**i**_{x}**h**, for this would be saying
'for all x the combination of x and **i**_{x} is **h**'. No, **h** must be allowed to
depend on x - to have x as a subscript. Our premise becomes

P_{5} = Rx**i**_{x}**h**_{x},

in words: "for all x there is an h such that h is equal to the combination of x and the inverse of x". (Indeed, this may be understood as a specialization of the more general axiom:

P_{0} = Rxy**z**_{xy}.)

Step 1. At last we can make the first step of our proof. This consists of resolving P_{4},
P_{5} and P_{3} with P_{1}. We can do this as a compound resolution,
as described above - a question of evaluating

Res(P_{4}, P_{5}, P_{3}, P_{1}).

The crucial thing is to unite the compound term consisting of the level -1 terms of P_{1}
with the product P_{4}P_{5}P_{3}, i.e.

Rxyu Ryzv Ruzw with R**i**_{p}p**e** Rqi_{q}**h**_{q} R**e**rr .

We calculate the unifying substitution as follows:

x =i_{p}y = p = q z =i_{q}=i_{p}= r u =ev =h_{q}=h_{p}w = r =i_{p}

This turns Rxvw (the consequence of P_{1}) into

R**i**_{p}**h**_{p}**i**_{p},

thus

Res(P_{4}, P_{5}, P_{3}, P_{1})
= R**i**_{p}**h**_{p}**i**_{p}.

Step 2. We calculate Res(P_{5}, R**i**_{p}**h**_{p}**i**_{p},
P_{5}, P_{2}). For this we must unite

Rxyu Ryzv Rxvw with
Rp**i**_{p}**h**_{p} R**i**_{q}**h**_{q}**i**_{q}
Rr**i**_{r}**h**_{r}.

We calculate the unifying substitution as follows:

x = p = r y =i_{p}=i_{q}∴ q = p z =h_{q}=h_{p}u =h_{p}v =i_{q}=i_{r}=i_{p}w =h_{r}=h_{p}

Therefore Ruzw (the conclusion) becomes

R**h**_{p}**h**_{p}**h**_{p},

which is eminently satisfactory, as it allows us to progress to

Step 3: Application of the lemma (stronger version), leading to E**e****h**_{p}.

Step 4: What can we do with E**e****h**_{p} ? Let examine the last stage of the
'natural language proof'. This hinges on the triple product

x•**i**_{x}•x

which is equal to both

(x•**i**_{x})•x and x•(**i**_{x}•x),

hence to

**h**_{x}•x and x•**e**.

This is where we might hope to make use of the equality of **h**_{x} and **e**. Surely, if
**h**_{x} and **e** are equal,
it is reasonable to infer that **h**_{x}•x is equal to **e**•x, equal in turn to x?
It's time for another axiom, which we will denote E_{2}:

That's pretty self-evident, isn't it? At any rate, putting E_{2} together with P_{3}
and E**e****h**_{x} we obtain the conclusion R**h**_{x}pp :

Step 5. We resolve P_{5}, P_{4} and the result just obtained, R**h**_{x}pp,
with P_{1}, which means unifying

Rxyu Ryzv Ruzw with Rp**i**_{p}**h**_{p}
R**i**_{q}q**e** R**h**_{r}ss.

We calculate the unifying substitution as follows:

x = p y =i_{p}=i_{q}∴ q = p z = q = s ∴ s = p u =h_{p}=h_{r}∴ r = p v =ew = s = p

Therefore

Rxvw = Rp**e**p.

Thus Res(P_{5}, P_{4}, R**h**_{x}pp, P_{1}) = Rp**e**p.

Step 6 (if felt necessary). Rp**e**p can be resolved with (R**aea**) to produce O - and our theorem
is proved - albeit with the help of the premises P_{5}, E_{1} and E_{2},
introduced along the way! ◊

There remains the small problem of showing that **i**_{x} behaves as a right-inverse, as well as
a left-inverse. What we want to derive is Rx**i**_{x}**e**. But by definition of **h**_{x},
we have Rx**i**_{x}**h**_{x}; and at step 3 we derived E**e****h**_{x}. Is that
not good enough? Well, not quite: we need another little axiom, another property of Exy, namely:

E_{3} = (Rabx Exy ( Raby )).

With the help of E_{3}, we are done◊

Don't miss the postscript (continues on another page...)