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.


[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.

  • 1
    $\begingroup$ 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$. $\endgroup$ – 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?


[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.


Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.