ConZF

A proof of the consistency of ZF in Lean 4, from excluded middle alone:

theorem PSet.con_ZF (em : ∀ p : Prop, p ∨ ¬p) : Con ZF
-- 'PSet.con_ZF' does not depend on any axioms

No Classical.choice, no propext, no Quot.sound; excluded middle is a hypothesis, not an axiom. ZF is the usual first-order theory (with the Separation and Replacement schemas), and Con is non-derivability of falsity in a Hilbert-style proof system. The development uses only PSet.{0} : Type 1, that is, two predicative universes. It does not depend on Mathlib, so that the axiom report is meaningful.

The point is that Replacement in the sets-as-trees model does not need a choice or description operator: large elimination of Acc over a carrier as big as the type of sets is enough. See doc/main.tex for the construction; CI builds it, and the current PDF is at releases/download/pdf/ConZF.pdf.

Build

lake build

(Lean toolchain as in lean-toolchain; no dependencies.)

Files

File	Content
ConZF/PSet.lean	sets as trees, bisimulation, membership, ∈-induction, basic operations, guards
ConZF/Mat.lean	the materializing recursion F (an Acc.rec on paths), coherent target assignments, materialize
ConZF/Repl.lean	replacement: images of functional relations with values in a class with uniform assignments
ConZF/Rule.lean	assignments generated by a one-node rule
ConZF/Pair.lean, Ord.lean, VLevel.lean	pairs, ordinals, rank, power set, the levels V_x, ω, the label set D
ConZF/Worldly.lean	the definability rule and dichotomy
ConZF/Fml.lean, Proof.lean	first-order formulas, satisfaction in class models, codes, the proof system, soundness
ConZF/ZF.lean, ZFRead.lean	the axioms of ZF, ZFModel, readback lemmas for the axioms
ConZF/FirstOrder.lean	the two models and con_ZF
ConZF/Uniform.lean	a single model, the sets of hereditarily good rank (hg_model, con_ZF')
ConZF/Stable.lean, Negative.lean	Con ZF from ¬¬EM; a probe of the negative translation and why Acc is the obstruction
ConZF/NatInstance.lean	an early sanity check (finite ordinals); not used