Undecidability results for restricted universally quantified formulae of set theory. (English) Zbl 0797.03005

Summary: The problem of establishing whether there are sets satisfying a formula in the first order set theoretic language \({\mathcal L}_ \in\) based on \(=\), \(\in\), which involves only restricted quantifiers and has an equivalent \(\forall\exists\)-prenex form (\((\forall\exists)_ 0\)-formula), is neither decidable nor semidecidable. In fact, given any \(\omega\)-model of \(\text{ZF}-\text{FA}\), where FA denotes the Foundation Axiom, the set of existential closures of \((\forall\exists)_ 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 \({\mathcal L}_ \in\). If satisfiability refers to \(\omega\)-models of \(\text{ZF}- \text{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.


03B25 Decidability of theories and sets of sentences
03E99 Set theory
03D35 Undecidability and degrees of sets of sentences
03D10 Turing machines and related notions
Full Text: DOI


[1] Non-well-founded sets, CSLI Lecture Notes, 1988.
[2] Breban, Adv. Appl. Math. 5 pp 147– (1984)
[3] Breban, Comm. Pure Appl. Math. 34 pp 177– (1981)
[4] , and , Set-theoretic reductions of Hilbert’s tenth problem, pp. 65–75 in: Proceedings Third Workshop ”Computer Science Logic,” Kaiserslautern, 1989, · Zbl 0925.03045
[5] , and , eds., Lecture Notes in Computer Science, Vol. 440, Springer-Verlag, Heidelberg, 1990.
[6] Cantone, Comm. Pure Appl. Math. 40 pp 37– (1987)
[7] and , Computability, Complexity, and Languages, Academic Press, New York, 1983.
[8] Parlamento, Comm. Pure Appl. Math 41 pp 221– (1988)
[9] Parlamento, Zeitscrift Math. Log. Grundlagen Math. 38 (1992)
[10] On a generalization of Herbrand’s theorem, Doctoral Dissertation, New York University, 1990.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.