Foundation Primitive Recognition Calculus Prcdistinction Dichotomy Not Degenerat

The distinction dichotomy

In logic and mathematics, a formal system is a set of symbols and rules for manipulating them. The Recognition Science framework asks a basic question about any such system: can it tell two of its own objects apart? The answer, proved as a theorem in the framework's machine-checked library of formal theorems, is a strict dichotomy. A system either has a discrimination relation that is empty, meaning it cannot distinguish any two objects, or it has at least one pair of objects it can tell apart. There is no third possibility.

The theorem not_degenerate_iff_discriminating states this equivalence precisely. A degenerate system, one whose discrimination relation is empty, is exactly a system that is not discriminating. The proof is a short exercise in logic: if a system is not degenerate, then by definition there exists a pair of objects it distinguishes, making it discriminating. Conversely, if it is discriminating, it cannot be degenerate, since the existence of a distinguished pair contradicts the claim that no pair is distinguished.

The dichotomy extends further. The framework proves that any formal system with a reflexive expression order, meaning every expression extends itself, is either degenerate or realizes a structure called the δ core. This δ core is a minimal embedding of the primitive recognition calculus into the system's own interface. The headline result, stated in the framework's library, is that distinction is not optional: the only system that escapes the δ core is the degenerate one, which cannot express a single non-trivial proposition.

The framework also checks that the named foundations of mathematics, logic, arithmetic, set theory, and type theory all fall on the discriminating side of this dichotomy. Each is non-degenerate and therefore realizes the δ core. This means the theorem is not an abstract curiosity; it applies to the systems that actually underpin mathematical practice.

What the theorem does not claim is just as important as what it proves. It does not say that any discriminating system is consistent or complete. It does not say that the discrimination relation must be decidable, or that the system must be able to distinguish every pair of objects. The theorem only establishes the minimal condition: at least one pair must be distinguishable for the system to be non-degenerate. A system that distinguishes exactly one pair and nothing else is still discriminating, and the theorem applies to it fully.

/-- Degeneracy and discrimination are exact negations. -/
theorem not_degenerate_iff_discriminating (F : FormalSystem) :
    ¬ Degenerate F ↔ Discriminating F := by
  constructor
  · intro h
    by_contra hc
    exact h (fun a b hab => hc ⟨a, b, hab⟩)
  · rintro ⟨a, b, hab⟩ hdeg
    exact hdeg a b hab

/-- **The dichotomy.** Any foundation with a reflexive expression order is either
degenerate or realizes δ. -/
theorem distinction_dichotomy (F : FormalSystem) (hrefl : ExprReflexive F) :
    Degenerate F ∨ RealizesDelta F := by
  by_cases h : Discriminating F
  · exact Or.inr (realizesDelta_of_discriminating F h hrefl)
  · exact Or.inl (fun a b hab => h ⟨a, b, hab⟩)

/-- The four named foundations (logic, arithmetic, set theory, type theory) all
fall on the δ side of the dichotomy: each is non-degenerate, hence realizes δ. -/
theorem named_foundations_not_degenerate :
    ¬ Degenerate InevitabilityInstances.boolLogicSystem
      ∧ ¬ Degenerate InevitabilityInstances.peanoSystem
      ∧ ¬ Degenerate InevitabilityInstances.setFoundationSystem
      ∧ ¬ Degenerate InevitabilityInstances.typeTheorySystem :=
  ⟨not_degenerate_of_realizesDelta _ InevitabilityInstances.boolLogicSystem_embeds_delta,
    not_degenerate_of_realizesDelta _ InevitabilityInstances.peanoSystem_embeds_delta,
    not_degenerate_of_realizesDelta _ InevitabilityInstances.setFoundationSystem_embeds_delta,
    not_degenerate_of_realizesDelta _ InevitabilityInstances.typeTheorySystem_embeds_delta⟩

What this page does not claim

The theorem does not claim that a discriminating system is consistent or complete. The theorem does not claim that the discrimination relation is decidable. The theorem does not claim that a system must distinguish every pair of objects to be non-degenerate.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCDistinctionDichotomy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: