Type theory with excluded middle proves consistency of ZF set theory
CIC + EM $\vdash$ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice
Logic in Computer Science
Summary
The paper shows that a certain kind of mathematical logic called type theory, even without some usual assumptions like choice, can still prove that standard set theory (ZF) is consistent. This means the foundations of set theory can be justified inside a type theory that only assumes excluded middle, a basic logical principle. The authors formalized their proof in the Lean theorem prover. Their technique involves a complex kind of recursion on well-founded sets, producing ordinals and models of set theory without extra axioms.
What this means in practice
- •For proof assistant developers: Formalize and verify set theory consistency inside type theories with minimal assumptions.
- •For foundations of mathematics teams: Build models of ZF set theory from type theory frameworks to analyze foundational assumptions.
A theory result. No direct application yet.
Authors
Mario Carneiro
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.