The Axiom of Double Complement and its opposites
Abstract
Powell introduced the Axiom of Double Complement (DCom) to give his double-negation interpretation of ZF into IZFRep. However, the consistency, strength, and compatibility of DCom remain open problems. This article aims to survey the compatibility and consistency strength of DCom, its consequence and opposites, which will be named NDCom and ADCom. We will also develop Lubarsky's Kripke models over CZF to derive these results. We will show that DCom proves the Powerset axiom over CZF and is independent of IZF. We will also show that ADCom does not add consistency strength over CZF, by modifying the construction of Lubarsky's model for CZF+lnot Pow. We will also show that DCom, ADCom, and NDCom are persistent under realizability under modest conditions.
Related
- An extension of Subcomplete Forcing Axiom which implies diamondsuit+
- ADDITIVITY AXIOM FOR THE TORSION FORMS AND HIGHER CHEEGER-MÜLLER/BISMUT-ZHANG THEOREM
- An axiom of unique reflection
- TRISDUCTION: A Linguistically, Topologically, and Mathematically Sealed Verification Architecture · Triaxial Orthogonality, Twelve-Gate Closure, the Quaternionic Completion, the Root Axiom, and the Master Pre-Sealed Proposition Ledger
- Existence of bases implies the axiom of choice, a foundation-free proof
BibTeX
@misc{jeon2026axiom,
title = {{The Axiom of Double Complement and its opposites}},
author = {Hanul Jeon and James E. Hanson},
howpublished = {arXiv},
year = {2026},
month = aug,
doi = {10.48550/arxiv.2606.00861},
eprint = {2606.00861},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2606.00861},
}
RIS
TY - UNPB
TI - The Axiom of Double Complement and its opposites
AU - Hanul Jeon
AU - James E. Hanson
PY - 2026
DA - 2026/08/29
PB - arXiv
DO - 10.48550/arxiv.2606.00861
UR - https://arxiv.org/abs/2606.00861
AB - Powell introduced the Axiom of Double Complement (DCom) to give his double-negation interpretation of ZF into IZF_Rep. However, the consistency, strength, and compatibility of DCom remain open problems. This article aims to survey the compatibility and consistency strength of DCom, its consequence and opposites, which will be named NDCom and ADCom. We will also develop Lubarsky's Kripke models over CZF to derive these results. We will show that DCom proves the Powerset axiom over CZF and is independent of IZF. We will also show that ADCom does not add consistency strength over CZF, by modifying the construction of Lubarsky's model for CZF+lnot Pow. We will also show that DCom, ADCom, and NDCom are persistent under realizability under modest conditions.
ER -