×

The lack of definable witnesses and provably recursive functions in intuitionistic set theories. (English) Zbl 0585.03025

Let \(ZFI_ R\), \(ZFI_ C\) be intuitionistic Zermelo-Fraenkel set theory formulated with Replacement, resp. Collection. It is known that \(ZFI_ R\) has the existence property. It is shown that \(ZFI_ C\) does not have the existence property. This remains true if one adds Dependent Choice and all true \(\Sigma_ 1\)-sentences of ZF. It is known that ZF and \(ZFI_ C\) have the same provably recursive functions. It is shown that this is not true for \(ZFI_ C\) and \(ZFI_ R\). (From the authors’ summary).
Reviewer: B.van Rootselaar

MSC:

03E70 Nonclassical and second-order set theories
03F50 Metamathematics of constructive systems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Beeson, M., Continuity in intuitionistic set theories, (Boffa, M.; van Dalen, D.; McAloon, K., Logic Colloquium 78 (1979), North-Holland: North-Holland Amsterdam), 1-52
[2] Chang, C. C.; Keisler, H. J., Model Theory (1973), North-Holland: North-Holland Amsterdam · Zbl 0276.02032
[3] Feferman, S., Some applications of the notions of forcing and generic sets, Fund. Math., 56, 325-345 (1965) · Zbl 0129.26401
[4] Fourman, M. P., Sheaf models for set theory, J. Pure Appl. Algebra, 19, 91-101 (1980) · Zbl 0446.03041
[5] Fourman, M. P.; Scott, D. S., Sheaves and logic, (Lecture Notes in Mathematics, Vol. 753 (1979), Springer-Verlag: Springer-Verlag Berlin), 302-401 · Zbl 0415.03053
[6] Freyd, P. J., On proving that 1 is an indecomposable projective in various free categories (1978), one-page preprint
[7] Friedman, H., Some applications of Kleene’s methods for intuitionistic systems, (Lecture Notes in Mathematics, Vol. 337 (1973), Springer-Verlag: Springer-Verlag Berlin), 113-170
[8] Friedman, H., The consistency of classical set theory relative to a set theory with intuitionistic logic, J. Symbolic Logic, 38, 315-319 (1973) · Zbl 0278.02045
[9] Friedman, H., Classically and intuitionistically provably recursive functions, (Lecture Notes in Mathematics, Vol. 669 (1978), Springer-Verlag: Springer-Verlag Berlin), 21-27 · Zbl 0396.03045
[10] Corrigendum, 26, 101 (1984) · Zbl 0539.03040
[11] Friedman, H.; Ščedrov, A., Large sets in intuitionistic set theory, Ann. Pure Appl. Logic, 27, 1-24 (1984) · Zbl 0544.03031
[12] Grayson, R., Heyting-valued models for intuitionistic set theory, (Lecture Notes in Mathematics, Vol. 753 (1979), Springer-Verlag: Springer-Verlag Berlin), 402-414 · Zbl 0419.03033
[13] Jech, T., Set Theory (1978), Academic Press: Academic Press New York · Zbl 0419.03028
[14] Levy, A., Definability in axiomatic set theory II, (Bar-Hillel, Y., Mathematical Logic and Foundations of Set Theory (1970), North-Holland: North-Holland Amsterdam) · Zbl 0218.02056
[15] Moschovakis, Y. N., Descriptive Set Theory (1980), North-Holland: North-Holland Amsterdam · Zbl 0433.03025
[16] Myhill, J., Some properties of intuitionistic Zermelo-Fraenkel set theory, (Lecture Notes in Mathematics, Vol. 337 (1973), Springer-Verlag: Springer-Verlag Berlin), 206-231
[17] Rogers, H., Theory of Recursive Functions and Effective Computability (1967), McGraw-Hill: McGraw-Hill New York · Zbl 0183.01401
[18] Schmerl, J. H.; Shelah, S., On power-like models for hyperinaccessible cardinals, J. Symbolic Logic, 37, 531-537 (1972) · Zbl 0278.02042
[19] Shelah, S., On models with power-like orderings, J. Symbolic Logic, 37, 247-267 (1972) · Zbl 0273.02036
[20] Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, (Lecture Notes in Mathematics, Vol. 344 (1973), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0275.02025
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.