infinity_modeled
plain-language theorem explainer
The axiom of infinity holds in Mathlib's ZF universe: von Neumann ω contains ∅ and is closed under successor n ↦ n ∪ {n}. Anyone citing the full-ZFC parse of the Primitive Recognition Calculus needs this fact; it is exactly what hereditarily finite set theory could not supply. The proof is a two-constructor term that packages Mathlib's omega_zero and omega_succ.
Claim. In the ZF universe (Mathlib $\mathrm{ZFSet}$ at universe level $0$), the von Neumann ordinal $\omega$ satisfies $\emptyset\in\omega$ and $\forall n\in\omega,\; n\cup\{n\}\in\omega$.
background
This module builds a faithful parse of full ZFC as a formal system for the Primitive Recognition Calculus (PRC). The carrier is the abbreviation ZF := ZFSet.{0}, Mathlib's cumulative hierarchy pinned at the smallest universe so it fits the Type-0 FormalSystem interface.
Earlier HF (hereditarily finite) parses could exhibit extensional distinction and ∅ ≠ {∅}, but they could not host an infinite set. The axiom of infinity is the missing piece: a set ω that contains the empty set and is closed under the von Neumann successor x ↦ insert x x (i.e. x ∪ {x}).
Mathlib already constructs ZFSet.omega with those two closure properties. The present declaration simply records them as a single conjunction in the PRC parse vocabulary.
proof idea
One-line term proof. The conjunction is introduced by the pair constructor: the left conjunct is Mathlib's ZFSet.omega_zero (∅ ∈ ω); the right is the lambda that applies ZFSet.omega_succ to any membership hypothesis, giving successor-closure. No local reasoning beyond packaging those two library facts.
why it matters
Downstream, set_theory_with_infinity_realizes_delta quotes this theorem as its first conjunct and pairs it with the δ-embedding of zfSystem, lifting the HF caveat that "infinity is not modelled." The packaged theorem full_zfc_realizes_delta then lists infinity_modeled as clause (iv) of the faithful ZFC parse: extensionality, ∅ ≠ {∅}, discrimination by genuine ZF difference, infinity, and a nonempty PRC embedding into zfSystem.
In the Recognition foundation stack this is the set-theoretic leg that shows classical ZFC (not merely HF) realizes the δ core. It does not itself touch the forcing chain T0–T8 or the J-cost identity; it only certifies that the ambient set theory used for the parse is strong enough to host infinite carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.