{"id":"arxiv/2609.23143","url":"https://arxiv.org/abs/2609.23143","tags":["math.LO","cs.LO"],"score":0,"title":"CIC + EM $\\vdash$ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice","domain":"math.LO","source":"arxiv","authors":["Mario Carneiro"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-09-19","reactions":{}}