Degenerate
plain-language theorem explainer
A formal foundation is degenerate when its discrimination relation is empty: no two tokens can be told apart. This is the trivial side of the PRC distinction dichotomy. Anyone proving that a named foundation (logic, Peano, ZF, type theory, toposes) realizes δ cites non-degeneracy. The body is a one-line universal quantification over the FormalSystem interface.
Claim. A formal system $F$ is degenerate when for every pair of tokens $a,b$ of $F$, $F$ does not distinguish $a$ from $b$. Equivalently, the discrimination relation of $F$ is empty.
background
The Primitive Recognition Calculus (PRC) studies when a foundation can host the atomic distinction δ. The carrier is FormalSystem: a minimal interface with token and expression types, a binary discrimination predicate on tokens, an expression-extension order, and a map from abstract endpoints into tokens.
Degeneracy is the extreme case in which discrimination never holds. Its dual is discrimination: existence of at least one distinguished pair. Downstream, realizing δ means an embedding of the two-point distinction into the foundation that preserves discrimination; that forces non-degeneracy.
The local module builds the dichotomy: any foundation with a reflexive expression order is either degenerate or realizes δ. Degeneracy is therefore the only escape hatch from δ, and it is mathematically sterile (no non-trivial proposition can be expressed).
proof idea
Pure definitional abbreviation. The predicate is the universal statement that distinguishes fails on every token pair. No lemmas are invoked; later theorems unfold or negate this Prop directly (e.g. via not_degenerate_iff_discriminating and not_degenerate_of_realizesDelta).
why it matters
This is the negative pole of the PRC distinction dichotomy (δ4 headline: distinction is not optional except for the degenerate foundation). Parent results include distinction_dichotomy, distinction_not_optional, not_degenerate_iff_discriminating, and not_degenerate_of_realizesDelta.
Concrete non-degeneracy theorems for named foundations land here: boolean logic, Peano arithmetic, set theory, type theory (named_foundations_not_degenerate), full ZF (zfSystem_not_degenerate), the topos of sets (toposSystem_not_degenerate), and the three-foundations package. Each shows the foundation sits on the δ side, so the atomic distinction is forced rather than optional.
In the broader Recognition forcing chain this underwrites that any usable foundation already contains the seed of recognition structure; only the empty-discrimination system escapes, and it cannot host physics or mathematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.