setFoundationSystem_embeds_delta
plain-language theorem explainer
The set-theoretic foundation built from ∅ ≠ univ on a one-point carrier admits a Primitive Recognition Calculus embedding of the δ core. Anyone arguing that δ is foundation-independent cites this instance alongside the logic, Peano, and type-theory cases. The proof is a one-line application of the generic two-distinct-primitives lemma.
Claim. There exists a PRC embedding into the set-theoretic formal system whose two distinguished tokens are $\emptyset$ and $\mathrm{univ}$ on a one-point domain (so $\emptyset \neq \mathrm{univ}$), preserving endpoint distinction and finite trace extension.
background
In the Primitive Recognition Calculus, a formal system is δ-capable when it can host a PRC embedding: a map of the two primitive endpoints and of finite traces that preserves endpoint distinction and trace extension. The structure PRCEmbeddingInto packages exactly those preservation laws.
The set-theoretic instance is the formal system obtained from any two distinguishable carriers via ofTwoDistinct. Here the carriers are $\emptyset$ and $\mathrm{univ}$ on Set Unit, the classical $0 = \emptyset$ versus $1 = {\emptyset}$ separation that opens the von Neumann hierarchy.
Upstream, the generic Item-4 lemma states that any foundation exposing two distinguishable primitives realizes the δ core: given $a_0 \neq a_1$, the two-distinct system admits a nonempty PRC embedding. That lemma is the sole engine of the present instance.
proof idea
One-line term proof. Instantiate the generic theorem that any two distinguishable primitives realize δ, feeding the concrete witnesses $\emptyset$, $\mathrm{univ}$, and the inequality $\emptyset \neq \mathrm{univ}$ on Set Unit. The set-foundation system is definitionally that two-distinct system, so the nonempty embedding transfers immediately.
why it matters
This is one of the four named-foundation instances that widen Item 4: logic ($\mathsf{true} \neq \mathsf{false}$), arithmetic ($0 \neq 1$), set theory ($\emptyset \neq {\emptyset}$), and type theory ($\mathbf{2}$). Downstream, named_foundations_embed_delta conjoins the four nonempty embeddings, and named_foundations_not_degenerate uses each embedding to place the corresponding system on the non-degenerate side of the δ dichotomy.
In the Recognition framework the point is structural, not notational: the primitive endpoint distinction is forced wherever a foundation can tell two tokens apart. The set-theoretic case anchors the claim in the standard $0/1$ start of the cumulative hierarchy, so δ is not an artifact of Boolean or Peano syntax alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.