AbstractThe problem of establishing whether there are sets satisfying a formula in the first order set theoretic language ℒ︁ϵbased on =,ϵ, which involves only restricted quantifiers and has an equivalent ∀∃‐prenex form ((∀∃)0‐formula), is neither decidable nor semidecidable. In fact, given any ω‐model ofZF – FA, whereFAdenotes the Foundation Axiom, the set of existential closures of (∀∃)0‐formulae true in the model is a productive set. Undecidability arises even when dealing with restricted universal quantifiers only, provided a predicateis_a_pair(x), meaning thatxis a pair of distinct sets, is added to ℒ︁ϵ. If satisfiability refers to ω‐models ofZF – FAin which a form of Boffa's antifoundation axiom holds, then semidecidability fails as well; in fact, given any such model, the set of existential closures of formulae involving only restricted quantifiers and the predicateis_a_pairwhich are true in it, is a productive set. These results are all proved by making use of appropriate codings of Turing machine comp