Certain Partial Conservativeness Properties of Intuitionistic Set Theory with the Principle of Double Complement of Sets

A. Vladimirov

Matematičeskie zametki, Tome 103 (2018) no. 3, pp. 372-391.

Résumé

The Zermelo–Fraenkel set theory with the underlying intuitionistic logic (for brevity, we refer to it as the intuitionistic Zermelo–Fraenkel set theory) in a two-sorted language (where the sort $0$ is assigned to numbers and the sort $1$, to sets) with the collection scheme used as the replacement scheme of axioms (the $ZFI2C$ theory) is considered. Some partial conservativeness properties of the intuitionistic Zermelo–Fraenkel set theory with the principle of double complement of sets ($DCS$) with respect to a certain class of arithmetic formulas (the class all so-called AEN formulas) are proved. Namely, let $T$ be one of the theories $ZFI2C$ and $ZFI2C + DCS$. Then 1) the theory $T+ECT$ is conservative over $T$ with respect to the class of AEN formulas; 2) the theory $T+ECT+M$ is conservative over $T+M^-$ with respect to the class of AEN formulas. Here $ECT$ stands for the extended Church's thesis, $M$ is the strong Markov principle, and $M^-$ is the weak Markov principle. The following partial conservativeness properties are also proved: 3) $T+ECT+M$ is conservative over $T$ with respect to the class of negative arithmetic formulas; 4) the classical theory $ZF2$ is conservative over $ZFI2C$ with respect to the class of negative arithmetic formulas.

Détail

Keywords: intuitionistic logic, Zermelo–Fraenkel axioms for set theory, intuitionistic Zermelo–Fraenkel set theory, recursive realizability, partial conservativeness properties.

Bibliographie

[1] A. G. Dragalin, Matematicheskii intuitsionizm. Vvedenie v teoriyu dokazatelstv, Nauka, M., 1979 | MR | Zbl

[2] S. Klini, R. Vesli, Osnovaniya intuitsionistskoi matematiki s tochki zreniya teorii rekursivnykh funktsii, Nauka, M., 1978 | MR | Zbl

[3] S. K. Klini, Vvedenie v metamatematiku, IL, M., 1957 | MR | Zbl

[4] T. Jech, Set Theory, Springer, Berlin, 2003 | DOI | MR | Zbl

[5] H. Friedman, “The consistency of classical set theory relative to a set theory with intuitionistic logic”, J. Symbolic Logic, 38 (1973), 315–319 | DOI | MR | Zbl

[6] W. C. Powell, “Extending Gödel negative interpretation to ZF”, J. Symbolic Logic, 40 (1975), 221–229 | DOI | MR | Zbl

[7] R. J. Grayson, “Heyting-valued models for intuitionistic set theory”, Applications of Sheaves, Lecture Notes in Math., 753, Springer, Berlin, 1979, 402–414 | DOI | MR | Zbl

[8] V. A. Lyubetskii, “Teoremy perenosa i algebra modalnykh operatorov”, Algebra i logika, 36:3 (1997), 282–303 | MR | Zbl

[9] V. Kh. Khakhanyan, “Predikaty realizuemosti dlya teorii mnozhestv s intuitsionistskoi logikoi”, Smirnovskie chteniya. Vtoraya mezhdunarodnaya konferentsiya, Izd-vo in-ta filosofii RAN, M., 1999, 71–72

[10] H. M. Friedman, A. Ščedrov, “The lack of definable witnesses and provably recursive functions in intuitionistic set theories”, Adv. in Math., 57:1 (1985), 1–13 | DOI | MR | Zbl

[11] H. Friedman, “Some applications of Kleene's method for intuitionistic systems”, Cambridge Summer School in Mathematical Logic, Lecture Notes in Math., 337, Springer, Berlin, 1973, 113–170 | DOI | MR | Zbl

[12] J. Myhill, “Some properties of intuitionistic Zermelo–Fraenkel set theory”, Cambridge Summer School in Mathematical Logic, Lecture Notes in Math., 337, Springer, Berlin, 1973, 206–231 | DOI | MR | Zbl

[13] V. Kh. Khakhanyan, “Teoriya mnozhestv i tezis Chercha”, Issledovaniya po neklassicheskim logikam i formalnym sistemam, Nauka, M., 1983, 198–208 | MR

[14] M. Beeson, “Continuity in intuitionistic set theories”, Logic Colloquium '78, Stud. Logic Found. Math., 97, North-Holland, Amsterdam, 1979, 1–52 | MR | Zbl

[15] A. G. Vladimirov, “Svoistva effektivnosti intuitsionistskoi teorii mnozhestv so skhemoi collection”, Matem. zametki, 89:5 (2011), 658–672 | DOI | MR | Zbl

[16] D. C. McCarty, Realizability and Recursive Mathematics, PhD Thesis, Oxford Univ. Press, Oxford, 1981

[17] C. McCarty, “Realizability and recursive set theory”, Ann. Pure Appl. Logic, 32:2 (1986), 153–183 | DOI | MR | Zbl

[18] M. Rathjen, “Realizability for constructive Zermelo–Fraenkel set theory”, Logic Colloquium '03, Lect. Notes Log., 24, Assoc. Symbol. Logic, La Jolla, CA, 2006, 282–314 | MR | Zbl

[19] M. Rathjen, “Choice principles in constructive and classical set theories”, Logic Colloquium '02, Lect. Notes Log., 27, Assoc. Symbol. Logic, La Jolla, CA, 2006, 299–326 | MR | Zbl

[20] M. Rathjen, “Metamathematical properties of intuitionistic set theories with choice principles”, New Computational Paradigms. Changing Conceptions of What is Computable, Springer, New York, 2008, 287–312 | MR | Zbl

[21] V. Kh. Khakhanyan, “Nevyvodimost printsipa uniformizatsii iz tezisa Chercha v intuitsionistskoi teorii mnozhestv”, Matem. zametki, 43:5 (1988), 685–691 | MR | Zbl