Varieties of regular semigroups with uniquely defined inversion

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.