Semigroup Identities, Proofs, and Artificial Intelligence

TL;DR

This paper explores algebraic identities in semigroups and groups, examining proof sequences, free models, and connections to Burnside's Problem, with implications for automated proof methods.

Contribution

It introduces methods to find proof sequences transforming identities and determines free models for specific identities, linking semigroup identities to group theory and computational proof challenges.

Findings

Free model for y ~ x^2yx^2 has order 32.

Identifies relations between identities and Burnside's Problem.

Proposes computational approaches to proof sequences in algebraic identities.

Abstract

It is known that if every group satisfying an identity of the form yx ~ xU(x,y)y is abelian, so is every semigroup that satisfies that identity. Because a group has an identity element and the cancellation property, it is easier to show that a group is abelian than that a semigroup is. If we know that it is, then there must be a sequence of substitutions using xU(x,y)y ~ yx that transforms xy to yx. We examine such sequences and propose finding them as a challenge to proof by computer. Also, every model of y ~ xU(x,y)x is a group. This raises a similar challenge, which we explore in the special case y ~ x^my^px^n. In addition we determine the free model with two generators of some of these identities. In particular, we find that the free model for y ~ x^2yx^2 has order 32 and is the product of D4 (the symmetries of a square), C2, and C2, and point out relations between such identities and Burnside's Problem concerning models of x^n= e.