zfSystem_exprReflexive
plain-language theorem explainer
Full ZFC, parsed as a FormalSystem, has a reflexive expression order: every expression extends itself under derivation-length comparison. Anyone assembling the distinction-dichotomy side for ZFC (non-degenerate, δ-realizing) cites this. The proof is immediate from reflexivity of ≤ on ℕ.
Claim. For the FormalSystem encoding of full ZFC (expressions are natural numbers, with extension given by derivation-length order $m \le n$), every expression $e$ extends itself: $\forall e,\; e\le e$.
background
Primitive Recognition Calculus compares foundations via a FormalSystem interface: tokens, expressions, a discrimination relation, an expression-extension order, and endpoint tokens. Expression reflexivity means every expression extends itself under that order; the upstream definition states this is the expected property of any "is-derivable-from" / "$\subseteq$" / "extends" relation.
The local module parses full ZFC into that interface. Tokens are a small carrier injected into the ZF universe; discrimination is genuine ZF extensional difference of represented sets; endpoints are the real $\emptyset$ and ${\emptyset}$; expressions are natural numbers ordered by derivation length (exprExtends m n means $m\le n$).
This lemma is the reflexivity half of that order on the ZFC parse.
proof idea
Term-mode one-liner. Unfold ExprReflexive on zfSystem: the goal is $\forall n:\mathbb{N},; n\le n$. Discharge each instance by Nat.le_refl. No ZF set theory is used; only the choice of expression order as ordinary natural-number order.
why it matters
The distinction dichotomy splits foundations into a degenerate side and a δ-realizing side. Full ZFC is meant to land on the δ side (non-degenerate, hence realizes δ), and the parse must satisfy the structural interface properties, including expression reflexivity. This theorem closes that interface obligation for the ZFC system.
It sits beside the sibling facts that the ZFC system is expressive and embeds δ. No downstream consumers are wired yet in the graph; the immediate role is to complete the FormalSystem well-formedness package for the ZFC parse inside the Primitive Recognition Calculus foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.