Undecidability in Weak Membership Theories
Dorella Bellé, Franco Parlamento · 2017
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.