IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCFullZFCParse
Embeds classical ZF set theory into the Primitive Recognition Calculus FormalSystem interface at universe level 0. Supplies an injective witness map, proves empty is distinct from its singleton, models infinity via ω, and shows ZF distinguishes sets exactly by inequality. Downstream foundations-parsing layers import this as a concrete expressive formal system. The module is mostly definitions plus elementary extensionality and infinity lemmas from Mathlib ZFC.
claimWorking in the ZF universe at the smallest type level, the module defines a formal system whose carriers are ZF sets, with distinction identified with inequality $x \neq y$. It exhibits an injective witness embedding, proves $\emptyset \neq \{\emptyset\}$ and $\omega \neq \emptyset$, and records that this system is expressive and embeds the primitive distinction structure $\Delta$.
background
Primitive Recognition Calculus treats a formal system as a carrier of tokens equipped with a distinction relation, so that recognition can be stated without committing to a particular logic. The sibling module on the distinction dichotomy supplies the abstract $\Delta$ interface that any such system must satisfy or embed.
This module pins the carrier to Mathlib's ZF sets at universe level 0, matching the FormalSystem interface which lives in Type. Distinction is taken to be ordinary inequality of sets. Standard ZF facts are recorded as recognition-facing lemmas: the empty set is extensionally distinct from its singleton, and the axiom of infinity supplies a nonempty inductive set $\omega$.
An injective witness map packages ZF inequality into the calculus's witness language, so that later layers can treat ZF as one concrete expressive system among others rather than as ambient metatheory.
proof idea
Definitional spine: alias the ZF universe, build zfWitness and the packaged zfSystem, then prove the interface obligations. Extensionality gives empty $\neq$ singleton and the corresponding distinction lemma. Infinity is imported from Mathlib ZFC to obtain $\omega \neq \emptyset$. Injectivity of the witness is by construction of the embedding. Expressiveness is the biconditional that two sets are distinguished iff unequal. The $\Delta$-embedding and reflexivity obligations are discharged by aligning ZF inequality with the dichotomy interface from the imported distinction module.
why it matters in Recognition Science
Gives the foundations stack a fully concrete, classical formal system that meets the PRC expressiveness and distinction-embedding requirements. The sole recorded consumer is PRCFoundationsParsed, which aggregates parsed foundation systems for higher recognition arguments. Without a ZF instance, the calculus would only have abstract dichotomy structure and no standard set-theoretic model to cite when comparing recognition strength to ordinary mathematics. The module sits in the Foundation domain of the forcing chain's ground layer: it does not force $\phi$, eight-tick structure, or $D=3$, but supplies the set-theoretic backdrop against which those later constraints are stated.
scope and limits
- Does not prove consistency of ZF or construct a model of ZF inside Lean beyond Mathlib's axiomatic ZFC API.
- Does not address choice, replacement strength, or large-cardinal extensions.
- Does not derive physical constants, J-cost uniqueness, or any T5–T8 forcing step.
- Does not claim ZF is the unique expressive FormalSystem, only one concrete instance.
- Does not parse or interpret arbitrary first-order ZF sentences beyond the packaged distinction interface.
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