Towards a pseudoequational proof theory

TL;DR

The paper introduces a new proof scheme for pseudoidentities that is sound and complete in many cases, advancing the understanding of pseudoidentity proof systems in algebraic structures.

Contribution

It presents a new, sound proof scheme for pseudoidentities and proves its completeness in various algebraic contexts, supporting a broader conjecture.

Findings

Scheme is complete for locally finite varieties

Scheme is complete for pseudovarieties of groups and completely simple semigroups

Scheme is complete when the pseudovariety is σ-reducible for x=y

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 when 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.