A DECISION PROBLEM FOR VARIETIES OF COMMUTATIVE SEMIGROUPS

For a first order formula P: for-all x1 ... for-all x(n) there exists y1 ... there exists y(m) (u(x1, ..., x(n), y1, ..., y(m)) = v(x1, ..., x(n), y1, ..., y(m))), where u and v are two words on the alphabet {x1, ..., x(n), y1, ..., y(m)}, and a finite set E of semigroup identities with xy = yx in it, we prove that it is decidable whether P follows from E, that is whether all the semigroups in the variety defined by E satisfy P.