Yet Another Paper on Group Theory Single Axioms

(it's only a temporary title)

First posted in June 2004, updated several times since.

This work (in progress) is toward showing that the there are no single axioms shorter or simpler than those previously known for group theory in terms of {product,inverse} and in terms of {division}.

An equation has size (length, vars), where length is the number of occurrences of operations and variables (including "="), and vars is the number of variables. For example, x * e = x has size (5,1).

Mace4 was used extensively to find couterexamples. A new option, the ability to search for ring models, was added to Mace4 for this work, and a new script was written to run a sequence of Mace4 jobs.

Abelian Groups

The answer for abelian groups is easy. The known single axioms are the shortest possible.

Tarski's axiom for abelian groups in terms of division has size (11,3) [Tarski-1938]

    x / (y / (z / (x / y))) = z.

None can be simpler, because three variables are required, and each variable must have an even number of occurrences.

For abelian groups in terms of product and inverse, we have an axiom of size (12,3) [McCune-1993]

    ((x * y) * z) * (x * z)' = y.

None can be simpler, because three variables are required, each variable must have an even number of occurrences, and there must be an occurrence of inverse.

Group Theory

Here are the simplest known axioms.

In terms of division, we have the size (19,3) axiom [Higman-Neumann-1952]:

    x / ((((x / x) / y) / z) / (((x / x) / x) / z)) = y.

Question: Is there a single axiom of size (11,3), (15,3), or (15,4)? We show below that there is not.

In terms of product and inverse, we have the size (20,3) axiom [Kunen-1992]:

    ((z * (x * y)')' * (z * y')) * (y' * y)' = x

and the size (18,4) axiom [McCune-1993]:

    y * (z * (((w * w') * (x * z)') * y))' = x.

Ken Kunen shows in [Kunen-1992] that the only possibility for simpler axioms is size (18,3). Below we look at all of the size (18,3) candidates and eliminate all but a few of them.

Properties of Single Equational Axioms

These apply to groups and subvarieties (and many other theories).

One side of the equation must be a variable, say x.
If alpha=x is a single axiom, neither the leftmost nor rightmost variable in alpha can be x. Otherwise there can be projection models.
The axiom must have at least three variables. Otherwise there can be nonassociative models.
If alpha=x is a single axiom in terms of product and inverse, then mirror(alpha)=x is also a single axiom. Therefore, we can ignore product/inverse candidates (delta * gamma) = x, with size(delta) > size(gamma).

Let these be known as the basic constraints.

Division

Summary. There are no group theory identities of size (11,3) satisfying the basic constraints. There are 71 group theory identies of sizes (15,3) and (15,4) satisfying those contraints, and all of them are elimintated by a single non-group structure of size 7 (which turns out to be the smallest nonassociative inverse loop).

Look here for details on how the candidates were generated and how the counterexample was found.

Product and Inverse

All candidates of size (18,3) satisfying the basic constraints were generated.

1,981,980 equations were generated, and 20,568 of those are group identites. Mace4 was used in various ways to find counterexamples, and 23 candidates remain.

Look here for details on how the candidates were generated and how the counterexamples were found.

References

[Higman-Neumann-1952]: G. Higman and B. H. Neumann. Groups as groupoids with one law. Publicationes Mathematicae Debrecen, 2:215--227, 1952.
[Kunen-1992]: K. Kunen. Single axioms for groups. J. Automated Reasoning, 9(3):291--308, 1992.
[McCune-1993]: W. McCune. Single axioms for groups and Abelian groups with various operations. J. Automated Reasoning, 10(1):1--13, 1993.
[Tarski-1938]: A. Tarski. Ein Beitrag zur Axiomatik der Abelschen Gruppen. Fundamenta Mathematicae, 30:253--256, 1938.