hfSystem_exprReflexive
plain-language theorem explainer
Hereditarily finite set theory, parsed as a formal system, has a reflexive expression order: every expression extends itself under derivation-length comparison. Anyone placing HF on the δ side of the distinction dichotomy cites this. The proof is the one-line term applying natural-number reflexivity of ≤.
Claim. Let $F$ be the hereditarily finite set-theory formal system (tokens and expressions coded by naturals, expression order $m \le n$). Then the expression-extension relation of $F$ is reflexive: for every expression $e$, $e$ extends $e$.
background
The Primitive Recognition Calculus distinction dichotomy classifies foundations by whether their interface is degenerate or realizes the δ core. A key interface property is expression reflexivity: every expression extends itself under the system's exprExtends relation (the natural "is-derivable-from" / "extends" order).
Here HF set theory is parsed into the FormalSystem interface: tokens and expressions are natural-number codes, discrimination is extensional inequality, endpoints are genuine ∅ (code 0) and {∅} (code 1), and expression order is derivation-length order $m \le n$, which preserves trace extension. Reflexivity of that order is exactly the claim.
Upstream, ExprReflexive F is defined as $\forall e,, F.\mathrm{exprExtends}, e, e$. The arithmetic fact used is ordinary reflexivity of $\le$ on $\mathbb{N}$.
proof idea
Term-mode one-liner. Unfolding the definition, the goal is $\forall n : \mathbb{N},, n \le n$. Supply the identity function on expressions and discharge each instance by Nat.le_refl. No case split or induction is required; the HF expression order is literally natural-number order.
why it matters
This is one of the elementary interface lemmas that put HF set theory on the δ side of the distinction dichotomy (non-degenerate, hence realizing δ). Sibling results in the same module establish expressiveness, a PRC embedding of δ, non-degeneracy, and the summary that HF realizes δ. Without reflexivity of expression order, the formal-system parse would not be a legitimate foundation interface under the dichotomy axioms.
In the broader Recognition Science foundation layer, the dichotomy separates systems that can host the primitive recognition calculus from those that collapse. HF is the standard set-theoretic witness on the productive side; this lemma is the cheapest structural check in that witness chain. No downstream consumers are recorded yet; the immediate consumers are the sibling non-degeneracy and realizes-δ theorems in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.