First posted in June 2004, updated several times since.
William McCune and Michael Kinyon
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.
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.
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)' = xand 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.
Look here for details on how the candidates were generated and how the counterexample was found.
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.