ABSTRACT
Let φ range over the collection of conjunctions of equalities with one inequality in the language with the constant Ø for the empty set and a binary operation w which, applied to any two sets x and y yields the result of adding y as an element to x. The satisfiability of sentences of the form ∀φ with respect to the theory NW, having the obvious axioms for Ø and w, is undecidable. The satisfiability of sentences of the form ∃∀φ with respect to the theory obtained by adding to NW the following equational consequences of the extensionality axiom: (E 1)x w y w z = x w y, is undecidable. General conditions on codings of Turing Machine computations into an equational language, which entail undecidability, are specified.
