three_foundations_realize_delta
plain-language theorem explainer
Hereditarily finite set theory, Martin-Löf type theory, and a topos-style categorical foundation each admit a primitive recognition calculus (PRC) embedding: each can host the δ-core endpoint distinction and finite trace extension. Cite this when comparing foundations under the FormalSystem interface, or when arguing that standard foundations sit on the δ side of the distinction dichotomy. The proof is a pure packaging term: the conjunction of the three individual embedding theorems.
Claim. There exist PRC embeddings into each of three foundations: hereditarily finite set theory, Martin-Löf type theory, and a topos-theoretic formal system. Concretely, the conjunction $\mathrm{Nonempty}(E_{\mathrm{HF}}) \wedge \mathrm{Nonempty}(E_{\mathrm{TT}}) \wedge \mathrm{Nonempty}(E_{\mathrm{Topos}})$ holds, where each $E$ maps the two primitive endpoints to distinguished tokens and preserves finite trace extension.
background
Primitive Recognition Calculus (PRC) isolates a minimal distinction core: two endpoints and finite traces that extend. A PRC embedding into a formal system is a structure that maps endpoints to tokens and traces to expressions while preserving the system's discrimination relation and expression-extension order.
The three target systems are parsed into a common FormalSystem interface. HF set theory takes tokens as HF codes, discriminates by extensional inequality, and sends endpoints to $\emptyset$ and ${\emptyset}$. MLTT takes tokens as closed terms of $\mathbf{2}$, with the two constructors as endpoints. The categorical parse uses global points of $\Omega$ (truth values), with $\top$ and $\bot$ as endpoints and inequality as discrimination.
Upstream, each parse already proves its own embedding theorem (HF, type theory, topos), each via an expressiveness witness that the FormalSystem embedding target lemma turns into a nonempty PRC embedding.
proof idea
Term-mode packaging only. The proof is the triple $\langle$ hfSystem_embeds_delta, ttSystem_embeds_delta, toposSystem_embeds_delta $\rangle$, which inhabits the three-way conjunction of Nonempty embeddings. No new algebra is done here; each conjunct was already established in its parse module by applying FormalSystemEmbeddingTarget_proved to the corresponding expressiveness hypothesis.
why it matters
This declaration is the joint statement that the three classical foundations, once parsed, all realize the δ core rather than collapsing distinction. It sits beside the sibling claims that the three foundations are non-degenerate and own their own distinction mechanisms, and next to the separate result that set theory with infinity also realizes δ.
In the Recognition Science foundation layer, the point is comparative: major foundations are not alternatives to the primitive recognition calculus; they contain it. That supports the broader forcing narrative in which δ-level distinction is prior to, and recoverable inside, set-theoretic, type-theoretic, and categorical language. No downstream consumers are wired yet (used_by is empty), so the result presently serves as a named checkpoint for the foundations-comparison block rather than a lemma inside a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.