×

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

The authors consider formulas in a first-order language for sets whose only non-logical symbols are the binary predicate symbols \(=\) and \(\in\), representing equality and membership, respectively, and which are in prenex normal form with the quantificational prefix of the form \(\exists^*\forall^*\).
The question at hand is whether or not such a formula is satisfiable in the standard cumulative set hierarchy \(V=\bigcup_\alpha {\mathcal P}(V_\alpha)\). The authors provide a semi-decision algorithm for this satisfiability problem.

MSC:

03B25 Decidability of theories and sets of sentences
03E99 Set theory
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Proceedings of the London Mathematical Society 30 pp 264– (1930)
[2] DOI: 10.1002/malq.19960420105 · Zbl 0836.03011
[3] The decision problem. Solvable classes of quantificational formulas (1979) · Zbl 0457.03005
[4] Set theory for computing. From decision procedures to declarative programming with sets (2001)
[5] DOI: 10.1002/cpa.3160340203 · Zbl 0465.03003
[6] The classical decision problem (1997)
[7] Combinatorics (1986) · Zbl 0595.05002
[8] Notre Dame Journal of Formal Logic 49 pp 55– (2008)
[9] Truth in V for *-sentences isdecidahle 71 pp 1200– (2006)
[10] Vicious circles 60 (1996)
[11] Non-well-founded sets 14 (1988)
[12] The satisfiability problem for the class * in a set-theoretic setting (1992)
[13] Expressing Infinity without Foundation 56 pp 1230– (1991) · Zbl 0744.03051
[14] Journal of Automated Reasoning 7 pp 271– (1991)
[15] Proceedings of the American Mathematical Society 108 (1990)
[16] DOI: 10.1090/S0002-9939-1988-0938682-2
[17] DOI: 10.1002/cpa.3160480908 · Zbl 0849.03009
[18] DOI: 10.1016/S0747-7171(06)80009-X · Zbl 0796.03009
[19] Unsolvable classes of quantificational formulas (1979) · Zbl 0423.03003
[20] Basic set theory (1979) · Zbl 0404.04001
[21] DOI: 10.1090/S0002-9939-97-03630-7 · Zbl 0857.03027
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.