Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-29T17:56:08.415Z Has data issue: false hasContentIssue false
  • English
  • Français

The Bernays-Schönfinkel-Ramsey class for set theory: semidecidability

Published online by Cambridge University Press:  12 March 2014

Eugenio Omodeo  and
Alberto Policriti
Eugenio Omodeo
Affiliation:
Dipartimento di Matematica e Informatica, Università di Trieste, 34127, Via Valerio 12/B, Italy. E-mail: [email protected]
Alberto Policriti
Affiliation:
Dipartimento di Matematica e Informatica, Università di Udine, 33100, Via Delle Scienze 206, Italy. E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

As is well-known, the Bernays-Schönfinkel-Ramsey class of all prenex ∃*∀*-sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are ∈ and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper.

Keywords

Satisfiabilitydecision and semi-decision algorithmscomputable set theory
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 75 , Issue 2 , June 2010 , pp. 459 - 480
Copyright
Copyright © Association for Symbolic Logic 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[Acz88]Aczel, P., Non-well-founded sets, CSLI Lecture Notes, vol. 14, CSLI, Stanford, CA, 1988.Google Scholar
[BM96]Barwise, J. and Moss, L., Vicious circles, CSLI Lecture Notes, vol. 60, CSLI, Stanford, CA, 1996.Google Scholar
[BP06]Bellè, D. and Parlamento, F., Truth in V for ∃*∀∀-sentences isdecidahle, this Journal, vol. 71 (2006), no. 4. pp. 1200–1222.Google Scholar
[BP08]Bellè, D. and Parlamento, F., Decidability of ∃*∀∀-sentences in HF, Notre Dame Journal of Formal Logic, vol. 49 (2008), no. 1. pp. 55–64.CrossRefGoogle Scholar
[B0I86]Bollobás, B., Combinatorics, Cambridge University Press, 1986.Google Scholar
[BGG97]Börger, Egon, Grädel, Erich, and Gurevich, Yuri, The classical decision problem, Perspectives in Mathematical Logic, Springer, 1997.CrossRefGoogle Scholar
[BFOS81]Breban, M., Ferro, A., Omodeo, E. G., and Schwartz, J. T., Decision Procedures for Elementary Sublanguages of Set Theory. II: Formulas involving Restricted Quantifiers, together with Ordinal, Integer, Map, and Domain Notions., Communications on Pure and Applied Mathematics, vol. 34 (1981), pp. 177–195.CrossRefGoogle Scholar
[COP01]Cantone, D., Omodeo, E. G., and Policriti, A., Set theory for computing. From decision procedures to declarative programming with sets, Monographs in Computer Science, Springer-Verlag, 2001.Google Scholar
[DG97]Dreben, B. and Goldfarb, W. D., The decision problem. Solvable classes of quantificational formulas, Addison-Wesley, Reading, MA, 1979.Google Scholar
[Lev79]Levy, A., Basic set theory, Perspectives in Mathematical Logic, Springer-Verlag, 1979.CrossRefGoogle Scholar
[Lew79]Lewis, H.R., Unsolvable classes of quantificational formulas, Addison-Wesley, Reading, MA, 1979.Google Scholar
[OPP93]Omodeo, E. G., Parlamento, F., and Policriti, A., A derived algorithm for evaluating ε-expressions over abstract sets, Journal of Symbolic Computation, vol. 15 (1993), no. 5–6, pp. 673–704, Special issue on Automatic Programming, Biermann, A. W. and Bibel, W. (eds.).CrossRefGoogle Scholar
[OPP96]Omodeo, E. G., Parlamento, F., and Policriti, A., Decidability of ∃*∀-sentences in membership theories, Mathematical Logic Quarterly, vol. 42 (1996), no. 1, pp. 41–58.CrossRefGoogle Scholar
[OP95]Omodeo, E. G. and Policriti, A., Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case, Communications on Pure and Applied Mathematics, vol. 48 (1995), no. 9–10. pp. 1123–1155, Special issue in honor of Schwartz, Jacob T..CrossRefGoogle Scholar
[PP88]Parlamento, F. and Policriti, A., The Logically Simplest Form of the Infinity Axiom, Proceedings of the American Mathematical Society, vol. 103 (1988), no. 1, pp. 274–276.CrossRefGoogle Scholar
[PP90]Parlamento, F. and Policriti, A., Note on: The Logically Simplest Form of the Infinity Axiom, Proceedings of the American Mathematical Society, vol. 108 (1990), no. 1.CrossRefGoogle Scholar
[PP91a]Parlamento, F. and Policriti, A., Decision procedures for elementary sublanguages of set theory: XIII. Model graphs, reflection and decidability, Journal of Automated Reasoning, vol. 7 (1991), pp. 271–284.CrossRefGoogle Scholar
[PP91b]Parlamento, F. and Policriti, A., Expressing Infinity without Foundation, this Journal, vol. 56 (1991), no. 4, pp. 1230–1235.Google Scholar
[PP92]Parlamento, F. and Policriti, A., The satisfiability problem for the class ∃*∀∀ in a set-theoretic setting, Technical report, 13/92. Università di Udine, Italy, 10 1992.Google Scholar
[PPR97]Parlamento, F., Policriti, A., and Rao, K. P. S. B., Witnessing Differences Without Redundancies, Proceedings of the American Mathematical Society, vol. 125 (1997), no. 2. pp. 587–594.CrossRefGoogle Scholar
[Ram30]Ramsey, F. P., On a problem of formal logic, Proceedings of the London Mathematical Society. vol. 30 (1930), pp. 264–286, Read on 12 13, 1928.CrossRefGoogle Scholar