zfSystem_expressive
plain-language theorem explainer
Full ZFC, parsed as a formal system for the Primitive Recognition Calculus, distinguishes its two endpoint tokens: the genuine empty set and its singleton differ by extensional membership. Anyone proving that ZFC contains the δ-core cites this expressivity fact. The argument is a one-line appeal to the already-proved extensional split between ∅ and {∅}.
Claim. The formal system that encodes full ZFC is expressive: it distinguishes the left and right endpoint tokens of the primitive distinction, realized as $\emptyset$ and $\{\emptyset\}$. Equivalently, there exists a set $z$ in the ZF universe such that $z\in\emptyset$ is not equivalent to $z\in\{\emptyset\}$.
background
In the Primitive Recognition Calculus, a formal system carries tokens, expressions, a discrimination relation, and two endpoint tokens. Expressivity means the system can tell those endpoints apart: discrimination holds between the left and right endpoint tokens. That is the first inevitability pass for any candidate host theory.
Here the host is full ZFC at the smallest universe level. Tokens inject into the ZF universe by a witness map; discrimination is genuine extensional difference of the represented sets (a member of one that fails to be a member of the other). The endpoints are the real empty set and its singleton, i.e. von Neumann 0 and 1.
The upstream lemma states that the distinction between $\emptyset$ and ${\emptyset}$ is genuinely extensional: they differ in the member $\emptyset$. That witness is exactly what expressivity demands for this ZFC parse.
proof idea
Unfolding expressivity for this system reduces to showing the endpoint tokens (standing for $\emptyset$ and ${\emptyset}$) are distinguished under the system's discrimination relation. By definition that is the existence of a ZF set $z$ whose membership in $\emptyset$ is not equivalent to membership in ${\emptyset}$. The proof is a one-line wrapper that applies the extensional-distinction lemma, which supplies $z=\emptyset$ and uses the standard ZF facts that nothing belongs to empty and that empty belongs to its singleton.
why it matters
Expressivity is the hypothesis required to embed the δ-core of the Primitive Recognition Calculus into full ZFC. The immediate parent theorem asserts that full ZFC contains the δ-core, obtained by feeding this fact into the general embedding-target construction. In the Recognition foundation, the primitive distinction between the two endpoints is the starting point of the forcing apparatus; showing that ordinary ZFC already separates those endpoints certifies that the calculus is not demanding exotic set theory. It closes the first inevitability pass for the ZFC parse and licenses downstream claims that the δ-structure sits inside classical foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.