The shortest single axioms for groups of exponent 4 (Q1343390)

The author returns to the study of single axioms for some varieties of groups, using the automated reasoning program OTTER [see his paper in J. Automated Reasoning 9, 291-308 (1992; Zbl 0794.20001); the paper by \textit{W. W. McCune}, ibid. 10, 1-13 (1994; Zbl 0794.20002) should also be consulted] as a ``reasoning assistant''. He concentrates on groups of finite even exponent \(> 2\), and especially on those of exponent 4, because exponent 2 groups [that is Boolean groups] and groups of finite odd exponent have been adequately dealt with by other authors. His main result is that there are precisely three single axioms, except for trivial modifications, that define the variety of groups of exponent 4 in terms of a binary operation, namely multiplication, involve 3 variables, and are of the form \(u = v\), with \(v\) of length 1 [that is to say just a variable] and \(u\) of length 17 [counting variable and operation symbols; the author prefers to count just the variables, which, in the absence of nullary operations, is entirely justifiable]. An elaborate search, using OTTER, shows that no shorter law will do, and that all other such laws reduce, by obvious transformations, to one of the three. The author claims in the introduction that the reviewer [Bull. Aust. Math. Soc. 23, 81-102 (1981; Zbl 0581.20003)=Selected Works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1076-1097] ``found a general scheme for single axioms for any variety of groups, but single axioms for exponent \(n\) groups produced as instances of this scheme are quite large''. Both these claims are not quite correct, as the reviewer's ``general scheme'' applies only to varieties of groups that can be defined by a finite set of laws; and for groups of exponent \(n\) the length remains linear in \(n\), not biquadratic in \(n\), as the author claims in Section 6, if the reviewer's scheme is applied as stated, namely with a binary multiplication and a unary inversion.