Is the existence of double complement of a set provable in Intuitionistic ZF?

Question

In Powell's article [1] he introduces the axiom of double complement, which says a double complement $\{x : \lnot\lnot(x\in A)\}$ is a set for any set $A$.

I can't find similar axiom from other references, even in the Friedman's article [2] on double negation interpretation over set theories. Hence it is natural to ask the relation between his axiom and other axioms of IZF. (Note: Powell consider the axiom of collection rather than the replacement in his article, but I will consider full IZF.)

I have made some attempts on this problem: if $f(\beta):=\sup\{\alpha\in\mathrm{On} : \lnot\lnot(\alpha<\beta)\}$ exists for each ordinal $\beta$, then the axiom of double complement holds: then $\{x\in V_{f(\operatorname{rank}(A))} : \lnot\lnot(x\in A)\}$ would be the double complement of $A$. (Here $V_\alpha := \bigcup_{\beta\in\alpha} \mathcal{P}(V_\beta)$ is a von Neumann hierarchy. Axiom of power set is necessary in my argument.) However checking $f(\beta)$ is a set is at least as hard as checking the axiom of double complement.

Forcing or realizability seems not helpful to me. This is because we need to generate a set whose double complement is proper class to prove the independence of the axiom of double complement, and it seems to need a proper-class sized name. However both methods just deal with set-sized names.

My question is: Is the axiom of double complement provable from full IZF? If not, is it indenpendent from IZF? Is the axiom of double complement related to the law of excluded middle? I would appreciate any help.

(Added in Jan 04, 2019: Realizability can be used to prove some non-classical principles are compatible with the axiom of double complement. In fact, if $V$ is a model of ZFC and $\mathcal{A}$ is a pca then the realizability model $V(\mathcal{A})$ validates the axiom of double complement.)

(Added in Jan 06, 2019) I recheck details of the proof of the above statement and I found my proof does not work. Beeson states we can prove the consistency of IZF + Double complement + Church's thesis via realizability in his book Foundations of Constructive Mathematics without proof. I do not know it really holds.

---

References

[1] Powell, William C. "Extending Gödel's negative interpretation to ZF." The Journal of Symbolic Logic 40.2 (1975): 221-229.

[2] Friedman, Harvey. "The consistency of classical set theory relative to a set theory with intuitionistic logic 1." The Journal of Symbolic Logic 38.2 (1973): 315-319.

Answer 1

A good question. Bear in mind that there can be no set x whose double complement is the universe. (Think about $\{y\in x: y \not\in y\}$). If you are thinking in terms of a cumulative hierarchy picture of constructive sets then what this is trying to tell you is that, for any x, there comes a stage by which all things notnotin x have appeared. And of course, once you have reached such a stage you obtain doublecomp x by separation. But [the rank of] this stage might increase so steeply with the rank of x that no effective proof can be given that there is such a stage. If you pursue this line of thought you will probably be able to come up with a kripke model in which lots of sets lack double complements. I'll have a think about it and get back.

Answer 2

This is not a full answer, but I think it is worth to mention: we can prove the theory CZF + Full separation + ￢Double complement is consistent!

The proof goes as follows: consider the Lubarsky's first model in 1. Let $\check{0}(\kappa)=\varnothing$ and $\check{1}(\kappa) = \{\check{0}\upharpoonright (\mathrm{On}\setminus\kappa)\}$. They will behave as 0 and 1 of the model. Furthermore, for each ordinal $\kappa$ define $$\check{1}_\kappa (\lambda ) = \begin{cases}\varnothing & \text{if }\kappa<\lambda\text{ and} \\ \{\check{0}\upharpoonright (\mathrm{On}\setminus\lambda)\} & \text{otherwise.}\end{cases}$$

I will claim that the element $x\in M_0$, defined by $x(\nu)=\{\check{1}\upharpoonright (\mathrm{On}\setminus\nu)\}$ for every ordinal $\nu$, has no double complement. First, it is tedious to check

$$\kappa \vDash \lnot\lnot (\check{1}_\nu \in x) \iff \forall \lambda \ge \kappa \exists \mu\ge\lambda : \mu\models \check{1}_\nu \in x$$ and the later statement holds: take any $\mu>\max(\lambda, \nu)$. Hence if $y\in M_0$ is a double complement of $x$, then it must contain every $\check{1}_\nu$, which is impossible. (In fact, we need to prove any $y\in M_\xi$ for any $\xi$ cannot be a double complement of $x$. However, its proof is not too different from my proof.)

However, my proof (if correct) has some unsatisfactory points. First, it requires the consistency of ZFC. Lubarsky proved that CZF + Full separation is equiconsistent with the second-order arithmetic [2]. I wonder CZF + Full separation + ￢Double complement is equiconsistent with Second order arithmetic. Kripke models seems not adequate to derive such kind of equiconsistency result (unless we form a Kripke model of CZF over CZF.) Second, it does not settle my original question: what happenes if we assume the axiom of power set?

---

(Added in Jan 24, 2019) I found that V. H. Hahanyan makes a bunch of result on the axiom of double complement over IZF (example). But most of his article is written in Russian so it is not easily accessible to me.

---

References

(1) Lubarsky, Robert S. "Independence results around constructive ZF." Annals of Pure and Applied Logic 132.2-3 (2005): 209-225.

(2) Lubarsky, Robert S. "CZF and Second Order Arithmetic ." Annals of Pure and Applied Logic 141.1-2 (2006): 29-34.