hfSystem_embeds_delta
plain-language theorem explainer
Hereditarily finite set theory, parsed via Ackermann codes, admits a Primitive Recognition Calculus embedding: the empty set and singleton empty set serve as distinguished endpoints. Anyone citing that classical foundations realize the δ core will use this. The proof is a one-line wrapper applying the general embedding-from-expressiveness theorem to the fact that ∅ ≠ {∅}.
Claim. There exists a PRC embedding of the $\delta$ core into hereditarily finite set theory (Ackermann-coded as a formal system): the endpoint map sends the two primitive endpoints to $\emptyset$ and $\{\emptyset\}$, and the system distinguishes those tokens.
background
Primitive Recognition Calculus (PRC) isolates a minimal distinction core $\delta$: two endpoints and finite traces that extend. A formal system realizes $\delta$ when there is a structure PRCEmbeddingInto mapping endpoints to tokens and traces to expressions while preserving distinction and trace extension.
Here the target is HF set theory packaged as a formal system: tokens and expressions are natural numbers (Ackermann codes), discrimination is numerical inequality, and the endpoints are code $0$ ($\emptyset$) and code $1$ (${\emptyset}$). Expression order is derivation-length order, which respects trace extension.
Upstream, a system is expressive when it distinguishes its two endpoint tokens. For HF that is simply $0 \neq 1$. The general lemma FormalSystemEmbeddingTarget_proved states that every expressive formal system admits a PRC embedding (built by PRCEmbeddingInto.ofExpressive).
proof idea
One-line wrapper. Apply FormalSystemEmbeddingTarget_proved to hfSystem and the already-proved fact hfSystem_expressive (namely $0 \neq 1$). That general theorem returns a witness of Nonempty (PRCEmbeddingInto hfSystem) by constructing the embedding from expressiveness alone.
why it matters
This is the set-theory leg of the claim that standard foundations each contain the $\delta$ core. Downstream, three_foundations_realize_delta conjoins this result with the type-theory and category-theory analogues: each of the three named foundations admits a PRC embedding. Locally it feeds hf_set_theory_realizes_delta, which packages extensionality, the von Neumann $0$/$1$ membership facts, discrimination-by-set-difference, and the embedding into one statement, and hfSystem_not_degenerate, which places HF on the non-degenerate side of the distinction dichotomy.
In the Recognition Science foundation layer this supports the thesis that $\delta$ is not an exotic primitive but is already realized inside ordinary set-theoretic distinction ($\emptyset \neq {\emptyset}$), before the forcing chain (T0–T8) builds J-cost, $\varphi$, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.