Foundation Primitive Recognition Calculus Prcinevitability Instances Bool Logic

The logical seed

Classical logic begins with a two-valued distinction: every proposition is either true or false, and the two are different. That difference, false ≠ true, is the first and most basic act of discrimination in the logical system. The Recognition Science framework formalizes this intuition into a precise mathematical claim: the logical carrier, the two-element type of booleans, contains within it the entire primitive recognition calculus, which the framework calls the δ core. The theorem boolLogicSystem_embeds_delta states this embedding exists, and it is proved in the framework's machine-checked library of formal theorems.

The construction is explicit. The framework defines a formal system, a structure with tokens, expressions, and a rule for distinguishing them, from any type with two distinct elements. For booleans, the tokens are the two values false and true, and the distinction is simply that they are not equal. Expressions are finite traces of these tokens, and one expression extends another when it is longer. This system is expressive: it can tell its two endpoints apart. The theorem then shows that this expressive system admits an embedding of the δ core, meaning the primitive recognition calculus is not an additional assumption layered on logic but is already present in logic's most basic operation.

The proof is a direct application of a general result: any foundation exposing two distinguishable primitives realizes the δ core. The boolean case is the concrete witness, the law of logic's own two-valued carrier. The framework also provides three further witnesses, the natural numbers with 0 ≠ 1, the set-theoretic empty set versus the singleton, and the type-theoretic two-element sum type, to show the distinction is not an artifact of booleans. The theorem named_foundations_embed_delta packages all four embeddings into a single statement.

What the theorem does not claim is equally important. It does not claim that boolean logic is the only foundation that embeds the δ core, nor does it claim that the embedding is a full faithful parse of logic into the recognition calculus. The framework's own documentation is explicit that these are honest small witnesses, not complete translations. The theorem establishes that the primitive distinction appears wherever two primitives can be told apart, but it says nothing about how much of logic, arithmetic, or set theory beyond that first distinction is captured by the embedding.

/-- **Item 4 (concrete).** The logical foundation contains the δ core:
distinguishing `true` from `false` is the primitive distinction, so the Law of
Logic's carrier admits a PRC embedding. -/
theorem boolLogicSystem_embeds_delta :
    Nonempty (PRCEmbeddingInto boolLogicSystem) :=
  FormalSystemEmbeddingTarget_proved boolLogicSystem boolLogicSystem_expressive

/-- A formal system built from any type with two distinct primitives. Tokens are
the type's elements, expressions are finite-trace lengths, and expression
extension is the length order. -/
def ofTwoDistinct {α : Type} (a₀ a₁ : α) (_hne : a₀ ≠ a₁) : FormalSystem where
  Token := α
  Expr := Nat
  distinguishes := fun x y => x ≠ y
  exprExtends := fun m n => m ≤ n
  endpointToken := fun e => if e.side = Side.left then a₀ else a₁
  traceExpr := Trace.length
  traceExpr_extends := fun h => length_le_of_extends h

/-- **Item 4 (generic).** Any foundation exposing two distinguishable primitives
realizes the δ core. -/
theorem two_distinct_realizes_delta {α : Type} (a₀ a₁ : α) (hne : a₀ ≠ a₁) :
    Nonempty (PRCEmbeddingInto (ofTwoDistinct a₀ a₁ hne)) :=
  FormalSystemEmbeddingTarget_proved _ (ofTwoDistinct_expressive a₀ a₁ hne)

/-- **Item 4, widened.** Four structurally different foundations, the logical
two-valued carrier, the arithmetic `0 ≠ 1`, the set-theoretic `∅ ≠ {∅}`, and the
type-theoretic `𝟚`, each realize the δ core. The primitive distinction is not an
artifact of one foundation's notation; it appears wherever two primitives can be
told apart. -/
theorem named_foundations_embed_delta :
    Nonempty (PRCEmbeddingInto boolLogicSystem)
      ∧ Nonempty (PRCEmbeddingInto peanoSystem)
      ∧ Nonempty (PRCEmbeddingInto setFoundationSystem)
      ∧ Nonempty (PRCEmbeddingInto typeTheorySystem) :=
  ⟨boolLogicSystem_embeds_delta, peanoSystem_embeds_delta,
    setFoundationSystem_embeds_delta, typeTheorySystem_embeds_delta⟩

What this page does not claim

The theorem does not claim that boolean logic is the only foundation embedding the δ core. The theorem does not claim a full faithful parse of logic into the recognition calculus. The theorem does not claim that the embedding captures anything beyond the primitive two-token distinction.

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/PRCInevitabilityInstances.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: