Discriminating
plain-language theorem explainer
A formal foundation is discriminating when its token carrier admits at least one pair the system can tell apart. The predicate is the positive half of the degeneracy/discrimination split used throughout the Primitive Recognition Calculus dichotomy. It is a one-line existential over the FormalSystem distinguishes relation, not a derived theorem.
Claim. A formal system $F$ is discriminating if there exist tokens $a,b$ in the token carrier of $F$ such that $F$ distinguishes $a$ from $b$.
background
The Primitive Recognition Calculus works with a minimal formal-system interface: carriers for tokens and expressions, a binary distinguishes relation on tokens, an expression-extension order, and a map from abstract endpoints into tokens. That interface is exactly what makes the primitive distinction $\delta$ visible inside an arbitrary foundation.
Discrimination is the positive counterpart of degeneracy. Degeneracy says no token pair is distinguished; discrimination says at least one pair is. The module then proves these are exact logical negations, and that any foundation whose expression order is reflexive is either degenerate or realizes $\delta$.
Local setting is the PRC distinction dichotomy: once expression order is reflexive (every expression extends itself), the ability to tell objects apart is no longer optional for any non-trivial foundation.
proof idea
Pure definitional abbreviation. The predicate unpacks as a single existential: there exist tokens $a,b$ such that the system's distinguishes relation holds on the pair. No lemmas are applied; downstream theorems case-split on this Prop or unpack the witness.
why it matters
This predicate is the case-split hinge for the module's main results. The dichotomy theorem states that any foundation with reflexive expression order is either degenerate or realizes $\delta$, proved by cases on discrimination. The $\delta_4$ headline (distinction is not optional) packages the equivalence of realizing $\delta$ with discrimination, the dichotomy, and the fact that realizing $\delta$ rules out degeneracy.
It also feeds the constructive direction: a discriminating foundation with reflexive expression order realizes the $\delta$ core by mapping primitive endpoints onto a distinguished token pair and collapsing traces to a fixed expression. In the Recognition forcing chain this is the formal-system side of why a non-trivial foundation cannot avoid primitive distinction; only the fully degenerate system escapes, and that system cannot express a non-trivial proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.