Decidability and completeness for open formulas of membership theories. (English) Zbl 0837.03007

Bellè, Dorella; Parlamento, Franco

Notre Dame J. Formal Logic 36, No. 2, 304-318 (1995).

Summary: We establish decidability, with respect to open formulas in the first order language with equality =, the membership relation \(\in\), the constant \(\emptyset\) for the empty set, and a binary operation \(w\) which, applied to any two sets \(x\) and \(y\), yields the result of adding \(y\) as an element to \(x\), of the theory NW having the obvious axioms for \(\emptyset\) and \(w\). Furthermore we establish completeness with respect to purely universal sentences of the theory NW+E+R obtained from NW by adding the Extensionality Axiom E and the Regularity Axiom R, and of the theory \(\text{NW+AFA}'\) obtained by adding to NW (a slight variant of) the Antifoundation Axiom AFA.

MSC:

03B25

Decidability of theories and sets of sentences

Keywords:

decidability; open formulas; completeness; extensionality axiom; regularity axiom; antifoundation axiom

References:

[1]	Aczel, P., Non-Well-Founded Sets , CSLI Lecture Notes, 1988. · Zbl 0668.04001
[2]	Bellè, D., and F. Parlamento, “Deciding unquantified formulae in weak membership theories,” Technical Report 14/92, Università di Udine, 1992.
[3]	Breban, M., A. Ferro, E. Omodeo and J. T. Schwartz, “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. · Zbl 0465.03003 · doi:10.1002/cpa.3160340203
[4]	Collins, G. E., and J. D. Halpern, “On the interpretability of arithmetic in set theory,” Notre Dame Journal of Formal Logic , vol. 11 (1970), pp. 477–483. · Zbl 0185.01601 · doi:10.1305/ndjfl/1093894080
[5]	Dreben, B., and W. D. Goldfarb, The Decision Problem. Solvable Classes of Quantificational Formulas , Addison Wesley, Reading, 1979. · Zbl 0457.03005
[6]	Lewis H. R., Unsolvable Classes of Quantificational Formulas , Addison Wesley, Reading, 1979. · Zbl 0423.03003
[7]	Montagna, F., and A. Mancini, “A minimal predicative set theory,” Notre Dame Journal of Formal Logic , vol. 35 (1994), pp. 186–203. · Zbl 0816.03023 · doi:10.1305/ndjfl/1094061860
[8]	Omodeo, E., F. Parlamento and A. Policriti, “Decidability of \(\exists^* \forall\)-sentences in membership theories,” Mathematical Logic Quarterly , forthcoming. · Zbl 0836.03011 · doi:10.1002/malq.19960420105
[9]	Parlamento, F., and A. Policriti, “Decision procedures for elementary sublanguages of set theory XIII: model graphs, reflection and decidability,” Journal of Automated Reasoning , vol. 7 (1991), pp. 271–284. · Zbl 0734.03006 · doi:10.1007/BF00243810
[10]	Parlamento, F., and A. Policriti, “Expressing infinity without foundation,” The Journal of Symbolic Logic , vol 56 (1991), pp. 1230–1235. JSTOR: · Zbl 0744.03051 · doi:10.2307/2275470
[11]	Parlamento, F., and A. Policriti, “The decision problem for restricted universal quantification in set theory and the axiom of foundation,” Zeitschrift für Mathematische Logik und Grundlangen der Mathematik, vol. 38 (1992), pp. 143–156. · Zbl 0794.03016 · doi:10.1002/malq.19920380110
[12]	Parlamento, F., and A. Policriti, “Undecidability results for restricted universally quantified formulae of set theory,” Communication on Pure and Applied Mathematics , vol. 46 (1993), pp. 57–73. · Zbl 0797.03005 · doi:10.1002/cpa.3160460104
[13]	Parlamento, F., A. Policriti and K. P. S. B. Rao, “Witnessing differences without redundancies,” Technical Report 23/93, Universitá di Udine, 1993. JSTOR: · Zbl 0857.03027 · doi:10.1090/S0002-9939-97-03630-7
[14]	Tarski, A., and W. Szmielew, “Mutual interpretability of some essentially undecidable theories,” p. 734 in Proceedings of the International Congress of Mathematicians , vol. 1, Cambridge University Press, Cambridge, 1950.
[15]	Tarski, A., A. Mostowsky and R. M. Robinson, Undecidable Theories , North-Holland, Amsterdam, 1953. · Zbl 0053.00401