IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCFullZFCParse
Pins Mathlib's ZF universe at the lowest type level and packages it as a FormalSystem for Primitive Recognition Calculus. Supplies injectivity of a witness map, emptiness-vs-singleton distinction, and infinity, then proves the resulting system is expressive, embeds the distinction relation, and is expression-reflexive. Downstream foundations parsing imports this as the concrete ZF instance.
claimWork in Mathlib's ZF universe $V$ at universe level $0$. Distinguish $\emptyset$ from $\{\emptyset\}$ extensionally; model Infinity so $\omega\neq\emptyset$. Build an injective witness $w:V\to\Delta$ and a formal system $\mathcal{Z}$ whose distinction relation coincides with $\neq$, is expressive, embeds $\Delta$, and is expression-reflexive.
background
Primitive Recognition Calculus treats a formal system as a carrier of tokens together with a distinction (inequality) relation and an expression map. The upstream module PRCDistinctionDichotomy supplies the dichotomy language that any such system must satisfy: either two tokens are identified or they are distinguished.
This module imports Mathlib's ZFC basic development and freezes the ZF cumulative hierarchy at Type (level 0), matching the FormalSystem interface. The ZF carrier is ordinary sets; the intended distinction is extensional inequality. Infinity is taken from the ZF axiom so that $\omega$ is a genuine infinite set, not empty.
Sibling constructions name a witness embedding from ZF sets into the ambient distinction space, then assemble zfSystem with the standard emptiness/singleton and infinity facts needed to certify that ZF really separates tokens.
proof idea
Definition-heavy module with short supporting lemmas. ZF is an abbreviation for the pinned Mathlib universe. empty_ne_singleton and the extensional variant are elementary set equalities; infinity_modeled and omega_ne_empty quote the Infinity axiom. zfWitness is built so that zfWitness_injective is immediate from the encoding. zfSystem packages carrier, distinction, and expression; distinguishes_iff_ne identifies distinction with $\neq$. Expressiveness, $\Delta$-embedding, and expression-reflexivity are then one-line consequences of injectivity plus the empty/singleton split.
why it matters in Recognition Science
Feeds PRCFoundationsParsed, which aggregates concrete formal systems that PRC can parse. Without a verified ZF instance at the correct universe level, the foundations layer cannot claim that classical set theory sits inside the recognition calculus as an expressive, distinction-faithful system. The module therefore closes the ZF branch of the "which foundations embed?" checklist rather than advancing the T0–T8 forcing chain directly. It is infrastructure: once zfSystem is expressive and embeds $\Delta$, later parsing theorems may treat ZF on equal footing with other pinned calculi.
scope and limits
- Does not prove consistency of ZF or any large-cardinal extension.
- Does not construct a model of ZF inside PRC; it only wraps Mathlib ZF as a FormalSystem.
- Does not address Choice, Replacement strength, or universe polymorphism beyond level 0.
- Does not derive physical constants, J-cost uniqueness, or forcing steps T5–T8.
- Does not claim the witness map is unique or canonical among all embeddings.
used by (1)
depends on (1)
declarations in this module (14)
-
abbrev
ZF -
theorem
empty_ne_singleton -
theorem
empty_distinct_singleton_extensionally -
theorem
infinity_modeled -
theorem
omega_ne_empty -
def
zfWitness -
theorem
zfWitness_injective -
def
zfSystem -
theorem
distinguishes_iff_ne -
theorem
zfSystem_expressive -
theorem
zfSystem_embeds_delta -
theorem
zfSystem_exprReflexive -
theorem
zfSystem_not_degenerate -
theorem
full_zfc_realizes_delta