hfSystem
plain-language theorem explainer
Hereditarily finite set theory is wired into the PRC formal-system interface: tokens and expressions are natural-number Ackermann codes, discrimination is code inequality, endpoints are ∅ and {∅} as codes 0 and 1, and expression order is derivation length. Anyone showing that set theory realizes the δ core cites this parse. The body is a direct structure instance; monotonicity of finite-trace length discharges the extension law.
Claim. The HF set-theory parse is the formal system with token and expression carriers $\mathbb{N}$ (Ackermann codes of hereditarily finite sets), discrimination relation $a \neq b$, expression-extension preorder $m \le n$, left and right endpoint tokens $0$ and $1$ (coding $\emptyset$ and $\{\emptyset\}$), and trace-to-expression map equal to finite-trace length, which is monotone under trace extension.
background
The PRC inevitability theorem works against a minimal formal-system interface: carriers for tokens and expressions, a discrimination relation on tokens, an expression-extension relation, endpoint tokens for the two sides of a primitive distinction, and a map from finite traces into expressions that respects extension. Upstream, a finite trace is empty or extended by one distinction act; its length counts those acts and is monotone under extension. The two sides are left and right.
This module supplies the set-theory leg of that interface. Hereditarily finite sets are coded by natural numbers (Ackermann coding). Membership and extensional equality live on those codes; the empty set is code 0 and the singleton of empty is code 1. The discrimination relation is written as bare inequality of codes; a sibling theorem later identifies that with genuine extensional set difference.
proof idea
Direct structure instance, not a derived proof. Token and Expr are both $\mathbb{N}$. Discrimination is $\neq$. Expression extension is $\le$. The endpoint map sends left to 0 and right to 1. The trace map is finite-trace length; the required monotonicity obligation is discharged by the upstream lemma that length is monotone under trace extension.
why it matters
This is the set-theory parse that the three-foundations theorems consume. Downstream, endpoint expressiveness is the trivial $0 \neq 1$; the embedding theorem then yields a nonempty PRC embedding into this system; the packaged faithfulness theorem records extensionality, empty-set and singleton facts, discrimination by genuine set difference, and the embedding together. At the foundations layer, the three named foundations (set theory, type theory, category theory) each realize the δ core and none is degenerate, with this parse as the set-theory conjunct. In the Recognition chain that is the claim that classical foundations do not escape the primitive distinction core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.