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

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.