Towards a pseudoequational proof theory

Abstract

A new scheme for proving pseudoidentities from a given set $\Sigma$ of pseudoidentities, which is clearly sound, is also shown to be complete in many instances, such as when $\Sigma$ defines a locally finite variety, a pseudovariety of groups, more generally, of completely simple semigroups, or of commutative monoids. Many further examples for which the scheme is complete are given when $\Sigma$ defines a pseudovariety V which is $\sigma$-reducible for the equation $x=y$, provided $\Sigma$ is enough to prove a basis of identities for the variety of $\sigma$-algebras generated by V. This gives ample evidence in support of the conjecture that the proof scheme is complete in general.