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

Omodeo, Eugenio; Policriti, Alberto

J. Symb. Log. 77, No. 3, 896-918 (2012).

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.

MSC:

03B25	Decidability of theories and sets of sentences
03E99	Set theory

Keywords:

satisfiability; prenex formula; decision algorithms; semi-decision algorithms; computable set theory

References:

[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