CIC + EM ⊢ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice
Abstract
The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of ZF. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of ZF, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some Vρ is already a model of ZF; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way ZF has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.
Related
- A toric approach to social choice theory
- Kinetic theory for Transformers and the lost-in-the-middle phenomenon
- The Type-I Seesaw as a Relativistic Fermionic Proximity Effect: Spectral Moments, EFT Consistency, and Sterile-Sector Reconstruction
- Completing the Meijer--Barnes K-function: the excluded case N<0
- Unbiased Treatment Effect Estimation under Network Interference via Neighborhood-Excluded Cross-Fitting
BibTeX
@misc{carneiro2026conzf,
title = {{CIC + EM $\vdash$ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice}},
author = {Mario Carneiro},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.23143},
eprint = {2609.23143},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.23143},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - CIC + EM ⊢ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice
AU - Mario Carneiro
PY - 2026
DA - 2026/09/19
PB - arXiv
DO - 10.48550/arxiv.2609.23143
UR - https://arxiv.org/abs/2609.23143
AB - The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of ZF. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of ZF, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some V_ρ is already a model of ZF; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way ZF has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.
ER -