zfSystem_embeds_delta
plain-language theorem explainer
Full ZFC, parsed as a formal system with genuine extensional discrimination, admits a nonempty PRC embedding of the δ core. Anyone arguing that classical set theory realizes the primitive recognition distinction cites this. The proof is a one-line wrapper: expressiveness of the ZFC parse (∅ and {∅} differ extensionally) feeds the general embedding-target theorem.
Claim. There exists a PRC embedding into the formal-system parse of full ZFC: maps of the two primitive endpoints and of finite traces into ZFC tokens and expressions that preserve the left/right endpoint distinction and finite trace extension.
background
In the Primitive Recognition Calculus a formal system is expressive when it distinguishes two designated endpoint tokens. A PRC embedding into such a system maps the two primitive endpoints and finite traces into the system's tokens and expressions while preserving distinction and the trace-extension order.
This module parses Mathlib's ZFSet universe into that interface. Tokens are a two-point carrier injected by a witness map into ZF sets; discrimination is genuine extensional difference of the represented sets; the endpoints are the actual empty set and its singleton; expression order is derivation length. Upstream, expressiveness of this parse is already proved from the classical fact that ∅ and {∅} differ by membership. The general result FormalSystemEmbeddingTarget_proved then asserts that every expressive formal system carries a nonempty PRC embedding.
proof idea
One-line wrapper. Instantiate the general theorem that every expressive formal system admits a PRC embedding on the full-ZFC parse, supplying the already-proved expressiveness fact (the endpoints ∅ and {∅} are extensionally distinct). That general theorem builds the embedding via the ofExpressive constructor.
why it matters
This is the embedding half of the claim that full ZFC realizes the δ core. Downstream, full_zfc_realizes_delta packages it with extensionality, ∅ ≠ {∅}, genuine discrimination, and the infinity axiom; set_theory_with_infinity_realizes_delta lifts the HF caveat by pairing infinity_modeled with this embedding; and zfSystem_not_degenerate places full ZFC on the non-degenerate side of the distinction dichotomy. In the Recognition Science foundation layer this shows classical set theory is not δ-blind: it contains the primitive endpoint distinction on which later forcing-chain and recognition-composition arguments rest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.