Towards a pseudoequational proof theory (Q1729826)

Summary: 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 \(\mathrm 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 \(\mathrm V\). This gives ample evidence in support of the conjecture that the proof scheme is complete in general.