eyeprolog

Inverses in a group are unique

If two elements both undo x, are they really different?

In a group every element has an inverse, and only one. This example gives x two candidate inverses, i and j, checks that one works on the left and the other on the right, and concludes that they name the same element.

Run it in the playground · Source

---

The question

A group is a set with an operation, an identity element e, and inverses: combining an element with its inverse gives e. A standard first theorem says inverses are unique. If i·x = e and x·j = e, then i = i·(x·j) = (i·x)·j = j.

---

The group table

group_op(e, X, X) :- element(X).
group_op(X, e, X) :- element(X).
group_op(i, x, e).
group_op(x, j, e).
group_op(j, x, e).
group_op(x, i, e).

group_op(A, B, C) means A·B = C. The identity rules say e changes nothing; the four facts make both i and j inverses of x.

---

The rules

leftInverse(A, B) :- group_op(B, A, e).
rightInverse(A, B) :- group_op(A, B, e).

sameInverse(A, B, C) :-
  leftInverse(A, B),
  rightInverse(A, C),
  sameTerm(B, C),
  (B \= C).

sameTerm/2 holds the conclusion of the algebraic argument above, stated as facts: sameTerm(i, j) and sameTerm(j, i). The rule reports pairs of different names for the same inverse.

---

The answer

eyeprolog examples/group-inverse-uniqueness.pl

sameInverse(x, i, j).
sameInverse(x, j, i).

---

The reason

step(sameInverse(x, i, j),
     rule(16),
     ['A' = x, 'B' = i, 'C' = j],
     [leftInverse(x, i), rightInverse(x, j), sameTerm(i, j), i \= j]).
step(leftInverse(x, i), rule(14), ['A' = x, 'B' = i], [group_op(i, x, e)]).
step(rightInverse(x, j), rule(15), ['A' = x, 'B' = j], [group_op(x, j, e)]).

i is a left inverse of x because i·x = e, j is a right inverse because x·j = e, and the identity of the two is the fact sameTerm(i, j).

---

The check

condition('C1', resolution, ok, 12).
condition('C5', re_decision, ok, 2).
verdict(checked).

All 12 rule and fact steps replay, and the two \= tests were recomputed and agreed. Nothing is trusted. Note what the check does and does not establish: the derivation is valid, but the algebra that justifies sameTerm(i, j) lives in a fact, not in the proof.

---

Try it

• Remove the two sameTerm(i, j) and sameTerm(j, i) facts. The program now prints nothing: the conclusion depended on them.
• Derive sameTerm/2 from the group laws instead of stating it. Which associativity facts would group_op/3 need?

Learn more in The Art of EyeProlog, Chapter 28.

This site is open source. Improve this page.