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.