Group Theory

A group is a nonempty set G in which multiplication is associative such that a two-sided identity e exists whose product with x is x and for which the two-sided inverse of x exists. To study group theory, one can use the following clauses; throughout the remainder of this paper, we use the notation of William McCune's program OTTER [McCune90, McCune91a], where `` | '' means or and `` - '' means not.

EQ(prod(e,x),x).	EQ(prod(x,inv(x)),e).
EQ(prod(x,e),x).	EQ(prod(prod(x,y),z),prod(x,prod(y,z))).
EQ(prod(inv(x),x),e).	EQ(x,x).

The last clause (for reflexivity) is included, for its presence is required when paramodulation is used. When attempting to prove that some set of equalities is an axiom system for group theory, except for the clause for reflexivity, one simply negates the given clauses.

Problem GT1, simple. If the square of every x is the identity, the group is commutative.

EQ(prod(x,x),e).

Problem GT2, moderate. Prove that the following equality (taken from Meredith [Meredith68] is a single axiom for groups in which the square of every x is the identity. In particular, using the single axiom, derive the axioms for groups (given earlier) and the axiom that asserts that the square of every element is the identity.

EQ(prod(prod(prod(x,y),z),prod(x,z)),y).

Problem GT3, moderate. Prove that [[x,y],y] = e when the cube of every x is e, where is the product of x, y, the inverse of x, and the inverse of y.

EQ(prod(x,prod(x,x)),e).

EQ(com(x,y),prod(x,prod(y,prod(inv(x),inv(y))))).

Problem GT4, moderate. Prove that the following equality axiomatizes group theory; the corresponding theorem, proved by William McCune using OTTER [McCune91b], is a new contribution to the literature.

EQ(prod(x,inv(prod(y,prod(prod(prod(z,inv(z)),inv(prod(u,y))),x)))),u).

Problem GT5, moderate. Prove that the following equality axiomatizes commutative group theory; this new single axiom was found by William McCune using OTTER [McCune91b].

EQ(prod(prod(prod(x,y),z),inv(prod(x,z))),y).

Problem GT6, never proved in a single run. Prove that the following equality axiomatizes commutative group theory; the result was verified by Ken Kunen [private correspondence] using OTTER as an assistant.

EQ(prod(inv(prod(inv(prod(inv(prod(x1,x2)),prod(x2,x1))),prod(inv(prod(z,y)),
prod(z,inv(prod(prod(v,inv(x)),inv(y))))))),x),v).

Problem GT7, hard. Prove that the Fibonacci group given by the following equalities is the cyclic group of order 29, where, for example, a(x) means the product of a and x and a1(x) means the product of the inverse of a and x. Instead, one can take the axioms for groups and add equalities that assert that, for seven elements, the product of the first two is the third, ..., and the product of the seventh and the first is the second.

EQ(a(b(x)),c(x)).	EQ(e(e1(x)),x).
EQ(b(c(x)),d(x)).	EQ(f(f1(x)),x).
EQ(c(d(x)),e(x)).	EQ(g(g1(x)),x).
EQ(d(e(x)),f(x)).	EQ(a1(a(x)),x).
EQ(e(f(x)),g(x)).	EQ(b1(b(x)),x).
EQ(f(g(x)),a(x)).	EQ(c1(c(x)),x).
EQ(g(a(x)),b(x)).	EQ(d1(d(x)),x).
EQ(a(a1(x)),x).	EQ(e1(e(x)),x).
EQ(b(b1(x)),x).	EQ(f1(f(x)),x).
EQ(c(c1(x)),x).	EQ(g1(g(x)),x).
EQ(d(d1(x)),x).