We show that the Axiom of Foundation, as well as the Antifoundation Axiom AFA, plays a crucial role in determining the decidability of the following problem. Given a first-order theory T over the language , and a sentence F of the form with quantifier-free in the same language, are there models of T in which F is true? Furthermore we show that the Extensionality Axiom is quite irrelevant in that respect.

We establish the decidability, with respect to open formulas in the first order language with equality =, the membership relation , the constant for the empty set, and a binary operation w which, applied to any two sets x and y, yields the results of adding y as an element to x, of the theory NW having the obvious axioms for and w. Furthermore we establish the completeness with respect to purely universal sentences of the theory , obtained from NW (...) by adding the Extensionality Axiom E and the Regularity Axiom R, and of the theory obtained by adding to NW (a slight variant of) the Antifoundation Axiom AFA. (shrink)