full_zfc_realizes_delta
plain-language theorem explainer
Full ZFC (Mathlib ZFSet) realizes the δ-core of Primitive Recognition Calculus: it is extensional, separates ∅ from {∅}, discriminates tokens by genuine set inequality, models infinity (ω with successor closure), and admits a PRC embedding. Anyone verifying that classical set theory can host the recognition distinction cites this packaging result. The proof is a five-component term assembling prior local lemmas.
Claim. Mathlib's ZF sets satisfy all of the following: (i) extensionality, $a=b$ if and only if $\forall z\,(z\in a\leftrightarrow z\in b)$; (ii) $\emptyset\neq\{\emptyset\}$; (iii) the ZF-parsed formal system distinguishes Boolean tokens exactly when their witness sets are unequal; (iv) $\emptyset\in\omega$ and $\omega$ is closed under $n\mapsto n\cup\{n\}$; and (v) there is a nonempty PRC embedding into that formal system.
background
Primitive Recognition Calculus (PRC) asks which formal systems can host a minimal distinction between two endpoints and finite trace extension. A FormalSystem supplies tokens, expressions, a discrimination relation, and an expression-order; a PRCEmbeddingInto maps the two endpoints and traces so that discrimination and extension are preserved.
This module parses full ZFC (Mathlib ZFSet at universe 0) into that interface. Tokens are Booleans injected via a witness map into ZF sets (the real $\emptyset$ and ${\emptyset}$); discrimination is genuine extensional difference, not token accident. The local lemmas already record extensionality, $\emptyset\neq{\emptyset}$, discrimination iff witness inequality, and the axiom of infinity on von Neumann $\omega$.
The infinity clause is the point of using full ZFC rather than hereditarily finite sets: $\omega$ contains $\emptyset$ and is closed under successor $x\mapsto x\cup{x}$.
proof idea
One-line term packaging. The five conjuncts are discharged by, respectively: Mathlib's ZFSet.ext_iff; the local lemma empty_ne_singleton (membership of $\emptyset$ in ${\emptyset}$ but not in $\emptyset$); distinguishes_iff_ne (discrimination unfolds to existence of a disagreeing member, rewritten by extensionality to set inequality); infinity_modeled (omega_zero and omega_succ); and zfSystem_embeds_delta (nonemptiness of a PRC embedding into the ZF-parsed system). No extra reasoning.
why it matters
This is the faithful-parse certificate for full ZFC inside PRC: classical set theory realizes the δ-core (extensionality, a hard two-point distinction, discrimination by real set difference, infinity, and a PRC embedding). It closes the FullZFCParse development by bundling the local facts into a single citation target.
In the Recognition foundation layer, the result shows that the primitive distinction is not an exotic demand: ordinary ZFC already hosts it, including the infinite carrier that HF set theory cannot supply. There are no recorded downstream dependents yet; the theorem stands as the packaged endpoint of the ZFC parse rather than an intermediate lemma in a longer forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.