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

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.

• Double complement does hold in $V(\mathcal{A})$. Say the rank of $x \in V(\mathcal{A})$ is the least $\alpha$ with $x \in V_\alpha (\mathcal{A})$. If $e \Vdash x = y$ for some $e$, then $x$ and $y$ have the same rank. Hence we can take the double complement of $z$ to be the set of $\langle 0, x \rangle$ where $x \in V_\alpha(\mathcal{A})$, with $\alpha$ the rank of $z$ and there exists $e \in \mathcal{A}$ with $e \Vdash x \in z$. – aws Jan 6 at 12:12

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.

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?

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.