Foundation Primitive Recognition Calculus Prcdistinction Dichotomy Distinction N

The dichotomy of distinction

In logic and mathematics, a foundation is the base system in which everything else is expressed, such as set theory or type theory. A formal system, in the framework's sense, is a foundation with tokens (objects) and expressions (claims about those objects). The declaration distinction_not_optional, proved in the framework's machine-checked library of formal theorems, establishes a dichotomy: any formal system with a reflexive expression order is either degenerate or realizes δ. A degenerate foundation distinguishes nothing, meaning it cannot tell any two tokens apart. A foundation that realizes δ contains a copy of the primitive recognition calculus (PRC), the framework's basic structure of recognition events, embedded into its own interface.

The theorem's three parts work together. First, a foundation realizes δ exactly when it can distinguish at least one pair of objects, so the ability to discriminate is equivalent to containing the primitive structure. Second, every foundation with a reflexive expression order is either degenerate or realizes δ, leaving no middle ground. Third, realizing δ rules out degeneracy, so the two cases are mutually exclusive. The hypothesis is mild: the named foundations, including logic, arithmetic, set theory, and type theory, all satisfy the reflexivity condition and all fall on the δ side of the dichotomy, as proved in named_foundations_not_degenerate.

The practical consequence is that distinction is not optional for any foundation that can express even one non-trivial proposition. The only foundation that escapes δ is the one that distinguishes nothing at all, which cannot express a single non-trivial proposition. This means the primitive recognition structure is not an arbitrary addition to a foundation but a necessary component of any that can do meaningful work. The theorem does not claim that every formal system is discriminating, nor that the PRC embedding is unique, nor that the dichotomy extends to systems without a reflexive expression order.

/-- A foundation distinguishes nothing: its discrimination relation is empty. It
cannot tell any two objects apart. -/
def Degenerate (F : FormalSystem) : Prop := ∀ a b : F.Token, ¬ F.distinguishes a b

/-- **δ4 headline: distinction is not optional, except for the degenerate
foundation.** For any foundation with a reflexive expression order: (i) it realizes
δ exactly when it can distinguish at least one pair of objects; (ii) it is either
degenerate or realizes δ; (iii) realizing δ rules out degeneracy. The only
foundation that escapes δ is the one that distinguishes nothing at all, which
cannot express a single non-trivial proposition. -/
theorem distinction_not_optional (F : FormalSystem) (hrefl : ExprReflexive F) :
    (RealizesDelta F ↔ Discriminating F)
      ∧ (Degenerate F ∨ RealizesDelta F)
      ∧ (RealizesDelta F → ¬ Degenerate F) := by
  refine ⟨⟨?_, ?_⟩, distinction_dichotomy F hrefl, not_degenerate_of_realizesDelta F⟩
  · intro h
    exact (not_degenerate_iff_discriminating F).mp (not_degenerate_of_realizesDelta F h)
  · intro h
    exact realizesDelta_of_discriminating F h hrefl

/-- **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 every formal system is discriminating. It does not claim that the PRC embedding is unique for a given foundation. It does not claim that the dichotomy extends to systems without a reflexive expression order.

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: