ZF
plain-language theorem explainer
Pins the working ZF universe to Mathlib's ZFSet at universe level 0, matching the Type-0 FormalSystem interface. Anyone building the full-ZFC parse of the δ core cites this as the carrier of sets, membership, and ω. It is a one-line abbreviation with no proof content.
Claim. Write $\mathrm{ZF}$ for Mathlib's $\mathrm{ZFSet}$ at universe level $0$. This is the fixed carrier of sets used throughout the full-ZFC parse (empty set, singletons, $\omega$, membership, extensionality).
background
The Primitive Recognition Calculus (PRC) asks which formal systems realize the δ core: a minimal distinction structure with two endpoints that can be told apart. Earlier HF (hereditarily finite) parses give extensional distinction of ∅ and {∅} but cannot model infinity. This module lifts that caveat by working in full ZFC via Mathlib's ZFSet.
The FormalSystem interface is fixed at Type 0, so the set universe must sit at the smallest universe level. ZF is that pinned carrier: sets, ∈, empty set, singleton, insert, and the von Neumann ω all live here. Downstream lemmas then prove ∅ ≠ {∅}, that discrimination is genuine extensional inequality, and that ω contains ∅ and is closed under successor.
proof idea
Pure abbreviation: ZF is defined to be ZFSet at universe level 0. No tactics, no lemmas, no proof obligations. All set-theoretic facts are inherited from Mathlib.SetTheory.ZFC.Basic.
why it matters
This alias is the carrier for the full-ZFC leg of the PRC foundations parse. It feeds empty_ne_singleton and empty_distinct_singleton_extensionally (von Neumann 0 ≠ 1), infinity_modeled and omega_ne_empty (axiom of infinity), distinguishes_iff_ne (discrimination equals set inequality), and the packaged theorems zfSystem, full_zfc_realizes_delta, and set_theory_with_infinity_realizes_delta.
Those results close the HF caveat: full ZFC over this universe realizes the δ core with infinity modelled, so the set-theory parse is no longer limited to finite sets. In the Recognition forcing chain this supplies a concrete, extensional formal system in which the primitive distinction (and its infinite iterate along ω) can be embedded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.