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.


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

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.

  • Is the bear you mention in the first line a grizzly bear? – Asaf Karagila Apr 6 at 22:06

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.