CIC + EM $\vdash$ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice
Mario Carneiro
math.LO
Sep 19, 2026 · v1
cs.LO
TL;DR
Formalizes in Lean 4 (without Mathlib) a proof that ZF's consistency follows from CIC plus excluded middle with 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 $\mathrm{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 $\mathrm{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 $\mathrm{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 $\mathrm{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.
Problem
It was expected that a dependent type theory with an impredicative Prop but no choice or description operator would be much weaker than ZF, since sets-as-trees validates Zermelo set theory but seemingly not Replacement. The question is the exact proof-theoretic strength of Lean's type theory with excluded middle but no choice.
Approach
Using Aczel's sets-as-trees interpretation, the authors introduce a 'materializing recursion' via large elimination of the accessibility predicate that computes any ordinal specified by a proposition through a well-founded tree. A definability rule collects all definable cofinal maps at once rather than choosing one, avoiding the axiom of choice. The full construction, including first-order syntax, a proof system, satisfaction, soundness, and consistency, is formalized in a Lean 4 package with no dependencies and no Mathlib.
Results
The consistency of ZF is proved from excluded middle as the only assumption, with no choice, propositional extensionality, or quotients; Lean reports con_ZF depends on no axioms (excluded middle enters only as a hypothesis). The double negation of excluded middle suffices, which reduces to not-not well-foundedness of membership and implies the double negation of Markov's principle.
