zfSystem
plain-language theorem explainer
Full ZFC is packaged as a FormalSystem whose tokens are Booleans injected into Mathlib's ZFSet, with discrimination by genuine extensional set difference. Anyone showing that set theory realizes the δ core cites this carrier. The definition wires tokens, natural-number expressions, endpoints ∅ and {∅}, and trace length into the PRC interface in one structure instance.
Claim. Define a formal system with token type $\mathrm{Bool}$, expression type $\mathbb{N}$, discrimination $a\mathrel{\mathrm{dist}}b$ iff the ZF sets named by $a$ and $b$ differ on some member, expression order $m\le n$, left/right endpoints mapped to $\mathrm{false}/\mathrm{true}$ (standing for $\emptyset$ and $\{\emptyset\}$), and the expression of a finite trace equal to its length.
background
The Primitive Recognition Calculus (PRC) needs a minimal formal-system interface: a token type, an expression type, a discrimination relation on tokens, an expression-extension order, and a map from the two sides of a primitive distinction to endpoint tokens. That interface is what the inevitability theorem consumes when it asks whether a system realizes the δ core.
Here the ZF universe is Mathlib's ZFSet pinned at universe level 0. A witness map sends the two Boolean tokens into that universe (the von Neumann 0 and 1: $\emptyset$ and ${\emptyset}$). Discrimination is not a token-level accident: two tokens are distinguished exactly when there exists a ZF set that belongs to one image and not the other, i.e., genuine extensional difference.
Traces are finite sequences of distinction acts; their length supplies the expression carrier order via ordinary $\le$ on $\mathbb{N}$. The two sides of a distinction (left/right) are the forced endpoints of the primitive act.
proof idea
Pure structure instance, not a proof. Token is Bool; Expr is ℕ. The discrimination field is the existential over ZF membership disagreement of the two witnessed sets. Expression extension is ≤. Endpoint tokens send left to false and right to true. Trace-to-expression is trace length, with the monotonicity obligation discharged by the existing length-vs-extends lemma on traces.
why it matters
This is the full-strength set-theory leg of the PRC parse. Downstream, expressiveness (endpoints distinguished), the embedding of δ into the system, expression reflexivity, and non-degeneracy are all stated about this carrier. Those facts package into the theorem that full ZFC realizes δ: extensionality, $\emptyset\ne{\emptyset}$, discrimination by real set difference, infinity modelled on $\omega$, and a nonempty PRC embedding.
The foundations-level corollary then lifts the HF caveat ("infinity not modelled") and records that set theory with infinity realizes δ. Without this definition there is no single object on which those theorems can sit; it is the parse target that makes the set-theory side of the distinction dichotomy concrete inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.