A new scheme for proving pseudoidentities from a given set Σ of
pseudoidentities, which is clearly sound, is also shown to be complete
in many instances, such as when Σ defines a locally finite variety, a
pseudovariety of groups or, more generally, of completely simple
semigroups. Many further examples when the scheme is complete are
given when Σ defines a pseudovariety V which is σ-reducible for the
equation x = y, provided Σ is enough to prove a basis of identities
for the variety of σ-algebras generated by V. This gives ample
evidence in support of the conjecture that the proof scheme is
complete in general.
(Joint work with O. Klíma, from Masaryk University, Brno, Czech Republic)