| Abstract: | The 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 of ZF – FA, where FA denotes 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 predicate is_a_pair(x), meaning that x is a pair of distinct sets, is added to ???. If satisfiability refers to ω-models of ZF – FA in 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 predicate is_a_pair which are true in it, is a productive set. These results are all proved by making use of appropriate codings of Turing machine computations in the set theoretic language. |
