Abstract:
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.
Keywords:intuitionistic logic, Zermelo–Fraenkel axioms for set theory, intuitionistic Zermelo–Fraenkel set theory, recursive realizability, partial conservativeness properties.
Fulltext:
PDF file (566 kB)
