The Bernays-Schönfinkel-Ramsey class for set theory: decidability. (English) Zbl 1251.03025

Summary: As proved recently, the satisfaction problem for all prenex formulae in the set-theoretic Bernays-Schönfinkel-Ramsey class is semi-decidable over von Neumann’s cumulative hierarchy. Here, that semi-decidability result is strengthened into a decidability result for the same collection of formulae.


03B25 Decidability of theories and sets of sentences
03E99 Set theory
Full Text: DOI Euclid


[1] Egon Börger, Erich Grädel, and Yuri Gurevich The classical decision problem , Perspectives in Mathematical Logic, Springer,1997. · Zbl 0865.03004
[2] D. Cantone, E. G. Omodeo, and A. Policriti Set theory for computing. From decision procedures to declarative programming with sets , Monographs in Computer Science, Springer-Verlag,2001. · Zbl 0981.03056
[3] A. Dovier, E. G. Omodeo, E. Pontelli, and G.-F. Rossi A language for programming in logic with finite sets , Journal of Logic Programming , vol. 28(1996), no. 1, pp. 1-44. · Zbl 0874.68056
[4] K. Kunen Set theory: an introduction to independence proofs , Studies in Logic and the Foundations of Mathematics, Elsevier,1983. · Zbl 0534.03026
[5] E. G. Omodeo and A. Policriti The Bernays-Schönfinkel-Ramsey class for set theory: Semidecidability , Journal of Symbolic Logic, vol. 75(2010), no. 2, pp. 459-480. · Zbl 1201.03007
[6] E. G. Omodeo, A. Policriti, and A. I. Tomescu Infinity, in short , Journal of Logic and Computation ,
[7] F. Parlamento and A. Policriti The logically simplest form of the infinity axiom , Proceedings of the American Mathematical Society , vol. 103(1988), no. 1, pp. 274-276. · Zbl 0681.03032
[8] F. P. Ramsey On a problem of formal logic , Proceedings of the London Mathematical Society , vol. 30(1930), pp. 264-286, read on December 13, 1928. · JFM 55.0032.04
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.