Undecidability results for restricted universally quantified formulae of set theory

Abstract

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.