TY - JOUR

T1 - Varieties of regular semigroups with uniquely defined inversion

AU - Araújo, João

AU - Kinyon, Michael

AU - Robert, Yves

N1 - info:eu-repo/grantAgreement/FCT/5876/147271/PT#
UIDB/00297/2020
PTDC/MAT-PUR/31174/2017
Grant 359872
Sem PDF conforme despacho

PY - 2019

Y1 - 2019

N2 - Inverse semigroups and completely regular semigroups share some nice properties and in a certain sense, they are the top success stories in semigroup theory.Therefore a reasonable goal is to find other classes of regular semigroups with the same nice shared properties and try to replicate the successful structure theories achieved for those two classes. Perhaps surprisingly, the semigroup literature is mute on examples of other classes of regular semigroups with the same nice properties, while semigroupists, for decades, voiced the metamathematical conviction of the hopelessness of such a goal. Our guess is that many have tried that approach, but always failed, thus unable to publish (the muteness of the literature) and convinced that the path leads to nowhere (the metamathematical conviction). The aim of this paper is to provide some mathematical content for that metamathematical conviction. In his celebrated theorem, K. Arrow wrote down the nice properties a voting system should have and then went on to prove that no system has those properties. We follow a similar path by writing down the nice common properties of inverse semigroups and of completely regular semigroups, and then show that, under some constraints, any variety having those nice properties is contained in one of the other two (if not in both). The proof of this theorem is by exhaustion: all possible varieties (under certain constraints) are written down, and each one is tested regarding the possession of the nice properties. Many pass the test, but then all of them turn out to be varieties of inverse or completely regular semigroups. This proof requires thousands of lemmas and was only possible because we used ProverX, a system aimed at playing in automated reasoning the same role GAP or MAGMA plays in symbolic computation. The paper ends with some problems for experts in semigroups, equational logic and computer science.

AB - Inverse semigroups and completely regular semigroups share some nice properties and in a certain sense, they are the top success stories in semigroup theory.Therefore a reasonable goal is to find other classes of regular semigroups with the same nice shared properties and try to replicate the successful structure theories achieved for those two classes. Perhaps surprisingly, the semigroup literature is mute on examples of other classes of regular semigroups with the same nice properties, while semigroupists, for decades, voiced the metamathematical conviction of the hopelessness of such a goal. Our guess is that many have tried that approach, but always failed, thus unable to publish (the muteness of the literature) and convinced that the path leads to nowhere (the metamathematical conviction). The aim of this paper is to provide some mathematical content for that metamathematical conviction. In his celebrated theorem, K. Arrow wrote down the nice properties a voting system should have and then went on to prove that no system has those properties. We follow a similar path by writing down the nice common properties of inverse semigroups and of completely regular semigroups, and then show that, under some constraints, any variety having those nice properties is contained in one of the other two (if not in both). The proof of this theorem is by exhaustion: all possible varieties (under certain constraints) are written down, and each one is tested regarding the possession of the nice properties. Many pass the test, but then all of them turn out to be varieties of inverse or completely regular semigroups. This proof requires thousands of lemmas and was only possible because we used ProverX, a system aimed at playing in automated reasoning the same role GAP or MAGMA plays in symbolic computation. The paper ends with some problems for experts in semigroups, equational logic and computer science.

KW - Completely regular semigroups

KW - Computational algebra

KW - Gap

KW - Inverse semigroups

KW - ProverX

UR - http://www.scopus.com/inward/record.url?scp=85081361303&partnerID=8YFLogxK

U2 - 10.4171/PM/2033

DO - 10.4171/PM/2033

M3 - Article

AN - SCOPUS:85081361303

VL - 76

SP - 205

EP - 228

JO - Portugaliae Mathematica

JF - Portugaliae Mathematica

SN - 0032-5155

IS - 2

ER -