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

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.