Single axioms for groups
type: Item
instance of: scholarly article
title: Single axioms for groups
zbMATH Open document ID: 0794.20001
DOI: 10.1007/BF00245293
author: Kenneth Kunen
published in: Journal of Automated Reasoning
publication date: 1994-08-25T00:00:00Z
review text: This paper demonstrates the difference of approach to proving certain mathematical facts by an oldfashioned mathematician [like the reviewer] and a mathematician versed in theorem proving by computers, and it illustrates the strength of the latter approach. The reviewer had found various single axioms that define the variety of groups in terms of a binary operation, namely multiplication or multiplication of inverses, and a unary operation, namely inversion [\textit{B. H. Neumann}, Bull. Aust. Math. Soc. 23, 81-102 (1981; Zbl 0581.20003), Ill. J. Math. 30, 295-300 (1986; Zbl 0581.20004)=Selected works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1076- 1097, 1098-1103]. The laws were of the form \(u=v\), where \(v\) had length 1 and \(u\) had length 18 and involved 4 variables; and the reviewer conjectured that these numbers could not be reduced. The author disproves these conjectures by exhibiting laws with \(u\) of length 18 in only 3 variables and with \(u\) of length 16 in 4 variables. These laws were found by the author and by \textit{W. W. McCune} [see the following review Zbl 0794.20002] using the automated theorem-proving program OTTER. The author first proves explicitly some known results, which were stated, without proof [``not very difficult to prove \dots We omit the proofs''] by \textit{G. Higman} and \textit{B. H. Neumann} [Publ. Math. 2, 215-221 (1953; Zbl 0050.25303) = Selected works of \textit{B. H. Neumann} and \textit{Hanna Neumann}, Winnipeg, Canada (1988; Zbl 0655.20001), Vol. V, 1069-1075]. For example, to prove the known result that at least 3 variables are needed in the laws, the author exhibits an elegant Moufang loop of order 10, which is, moreover, boolean: this, apparently the smallest properly non-associative di-associative loop, was also found using a computer program. The computer was also extensively used to prove other results contained in the literature, for example that at le…
Mathematics Subject Classification ID: 20A05
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 20-04
zbMATH DE Number: 444945
zbMATH Keywords: single axioms
zbMATH Keywords: variety of groups
zbMATH Keywords: binary operation
zbMATH Keywords: unary operation
zbMATH Keywords: laws
zbMATH Keywords: length
zbMATH Keywords: variables
zbMATH Keywords: automated theorem-proving program OTTER
zbMATH Keywords: Moufang loop
zbMATH Keywords: non-associative di-associative loop
zbMATH Keywords: inversions
reviewed by: B. H. Neumann
describes a project that uses: OTTER
MaRDI profile type: Publication
Wikidata QID: Q114694848
cites work: Another single law for groups
cites work: Yet another single law for groups
Recommended article: Single axioms for groups and abelian groups with various operations
Recommended article: The shortest single axioms for groups of exponent 4
Recommended article: On single-law definitions of groups
Recommended article: Another single law for groups
Recommended article: Yet another single law for groups
Recommended article: Computer and Human Reasoning: Single Implicative Axioms for Groups and for Abelian Groups
Recommended article: Q4255507
Recommended article: Searching for shortest single axioms for groups of exponent \(6\)
Recommended article: Solution of the Robbins problem
Recommended article: Q3699030
description: scientific article; zbMATH DE number 444945