distinguishes_iff_extensional
plain-language theorem explainer
Two natural-number codes are distinguished by the HF formal system exactly when they differ on some Ackermann membership bit. Anyone packaging the HF parse as a realization of the δ core cites this equivalence. The proof rewrites distinction as inequality, applies bit-extensionality, and pushes the negation.
Claim. For all codes $a,b\in\mathbb{N}$, the HF formal system distinguishes $a$ from $b$ if and only if there exists an index $i$ such that membership of $i$ in $a$ fails to match membership of $i$ in $b$ (under Ackermann coding).
background
This module parses hereditarily finite set theory into the Primitive Recognition Calculus FormalSystem interface. Tokens and expressions are natural numbers under the standard Ackermann coding of HF sets: the code $n$ has member $i$ precisely when bit $i$ of $n$ is set (Mem).
Extensionality is already proved as bit-extensionality of $\mathbb{N}$: two codes are equal iff they have the same members (ext_iff). The HF system hfSystem takes tokens to be these codes and defines discrimination simply as inequality of codes, with endpoints the genuine empty set (code 0) and singleton-of-empty (code 1).
The local goal is to show that this inequality-based discrimination is not a coding accident: it coincides with genuine set-theoretic difference of membership.
proof idea
Unfold hfSystem.distinguishes to ordinary inequality $a\neq b$. Rewrite via ne_eq and the upstream extensionality theorem ext_iff, which states $a=b$ iff $\forall i,,(\mathrm{Mem},i,a\leftrightarrow\mathrm{Mem},i,b)$. Push the negation through the universal quantifier to obtain an existential witness of mismatched membership, then close by reflexivity.
why it matters
This lemma is the discrimination clause in the packaged faithful parse hf_set_theory_realizes_delta, which asserts that Ackermann-coded HF set theory satisfies extensionality, has the correct empty and singleton endpoints, discriminates by genuine set difference, and realizes the δ core via a nonempty PRC embedding.
In the Recognition foundation, the Primitive Recognition Calculus needs a concrete formal system whose distinction relation is not an arbitrary token predicate but the foundation's own extensional inequality. Citing this equivalence lets downstream work treat HF discrimination as set difference, aligning the parse with the von Neumann 0 and 1 endpoints and with the forcing-chain demand that recognition rest on genuine distinguishability rather than coding artifacts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.