The Axiom of Double Complement and its opposites

Powell introduced the Axiom of Double Complement ($\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$) to give his double-negation interpretation of $\mathsf{Z}\mathsf{F}$ into $\mathsf{I}\mathsf{Z}{\mathsf{F}}_{\mathsf{R}\mathsf{e}\mathsf{p}}$. However, the consistency, strength, and compatibility of $\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$ remain open problems. This article aims to survey the compatibility and consistency strength of $\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$, its consequence and opposites, which will be named $\mathsf{N}\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$ and $\mathsf{A}\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$. We will also develop Lubarsky’s Kripke models over $\mathsf{C}\mathsf{Z}\mathsf{F}$ to derive these results. We will show that $\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$ proves the Powerset axiom over $\mathsf{C}\mathsf{Z}\mathsf{F}$ and is independent of $\mathsf{I}\mathsf{Z}\mathsf{F}$. We will also show that $\mathsf{A}\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$ does not add consistency strength over $\mathsf{C}\mathsf{Z}\mathsf{F}$, by modifying the construction of Lubarsky’s model for $\mathsf{C}\mathsf{Z}\mathsf{F}+\mathsf{\neg }\mathsf{P}\mathsf{o}\mathsf{w}$. We will also show that $\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$, $\mathsf{A}\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$, and $\mathsf{N}\mathsf{D}\mathsf{C}\mathsf{o}\mathsf{m}$ are persistent under realizability under modest conditions.