hfSystem_expressive
plain-language theorem explainer
Hereditarily finite set theory, cast as a formal system, distinguishes its two primitive endpoints ∅ and {∅}. Anyone embedding the δ-core of Primitive Recognition Calculus into HF cites this as the expressiveness hypothesis. The proof is a one-line decidability check that the endpoint codes 0 and 1 are unequal.
Claim. The formal system of hereditarily finite sets is expressive: it distinguishes its left and right endpoint tokens, i.e. $\emptyset \neq \{\emptyset\}$.
background
Primitive Recognition Calculus packages candidate foundations as a FormalSystem: a token type, an expression type, a discrimination relation, an expression-extension order, and a map sending the two primitive endpoints (left/right) to tokens. A system is expressive when those two endpoint tokens are distinguished.
Here the system is HF set theory. Tokens are natural-number codes for hereditarily finite sets; discrimination is ordinary inequality of codes (extensional set inequality); the endpoints are the genuine empty set (code 0) and the singleton of empty (code 1). Expression order is derivation-length order, which preserves trace extension.
Upstream, expressiveness is defined exactly as distinguishing the two endpoint tokens. The local module parses HF into that interface so that PRC embedding theorems can be stated uniformly.
proof idea
Unfolding expressiveness on hfSystem reduces the claim to inequality of the two endpoint codes: $0 \neq 1$ in $\mathbb{N}$. The proof exhibits that goal and discharges it by decide. No set-theoretic lemmas are needed beyond the endpoint assignment in the HF formal-system record.
why it matters
This is the expressiveness gate for the HF parse of PRC. Downstream, hfSystem_embeds_delta applies the generic embedding-target lemma with this fact to conclude that HF set theory contains the δ core (a nonempty PRC embedding into HF). That step is the set-theoretic realization of the primitive distinction: the first inevitability pass requires a host that can tell the two endpoints apart. In the Recognition forcing chain this sits at the foundation layer, before J-uniqueness (T5), φ, the eight-tick octave, and $D=3$. It closes the HF branch of the "which formal systems realize δ" checklist in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.