Foundation Categorical Logic Realization

Categorical realization

In mathematics, a natural-number object (NNO) is a categorical way to say what the counting numbers are without relying on a pre-existing set theory. It is a structure with a zero element and a successor operation, plus a universal property: any other such structure receives a unique structure-preserving map from it. This is often called the Lawvere natural-number object, after William Lawvere, who isolated the idea in the 1960s. The key point is that the NNO is initial: it is the most basic, universal example, and every other arithmetic structure is a quotient or an extension of it.

The Recognition Science framework builds arithmetic from logic itself, using a construction called logic natural numbers: a discrete record of counting events generated by a zero and a successor step. The module CategoricalLogicRealization shows that this logical construction is not a separate, ad hoc number system. It packages the logic natural numbers as a Lawvere-style NNO, complete with the required initiality condition, decidable equality, and a nontrivial element. In plain language, the module proves that the numbers the framework derives from pure logic are exactly the same universal counting object that category theory identifies as the natural-number object.

The module also provides an explicit interface for what a full categorical realization would need: a category with objects, morphisms, a terminal object, and a designated NNO with zero and successor morphisms. It then shows that the logic natural numbers satisfy this interface. The bridge is deliberately lightweight: it does not rebuild category theory, but it names the data that a full categorical treatment would instantiate. This is a deliberate scoping choice, not a gap.

The central result is an invariance theorem: categorical arithmetic is the same no matter which realization of the natural numbers you start from. The module constructs a canonical realization from the logic natural numbers and then proves that for any other realization, the underlying carrier of the natural numbers is equivalent. In plain terms, if you build arithmetic from logic, you get the same counting structure as if you built it from any other valid starting point. The machine-checked library of formal theorems records this as a formal equivalence, so the claim is not a matter of informal argument but of verified proof.

What this changes for the framework: it ties the logical foundation of arithmetic to a well-established categorical concept, so that the natural numbers are not a framework-specific invention but a universal mathematical object. For the reader, it means that the arithmetic used throughout Recognition Science is the same arithmetic that any category theorist would recognize, and the framework's logical construction is one legitimate way to instantiate it.

/-- The canonical Lawvere NNO supplied by `LogicNat`. -/
def logicNatNNO : LawvereNNO.{0} where
  object := ArithmeticOf.logicNatPeano
  initial := ArithmeticOf.logicNat_initial
  decEq := (inferInstance : DecidableEq ArithmeticFromLogic.LogicNat)
  nontrivial := by
    refine ⟨ArithmeticFromLogic.LogicNat.succ ArithmeticFromLogic.LogicNat.zero, ?_⟩
    intro h
    exact (ArithmeticFromLogic.LogicNat.zero_ne_succ ArithmeticFromLogic.LogicNat.zero) h.symm

theorem logicNatNNO_has_category_interface :
    Nonempty (categoryInterfaceOfLawvere logicNatNNO).initiality :=
  ⟨trivial⟩

/-- Categorical arithmetic is invariant with every realization. -/
noncomputable def categorical_arithmetic_invariant (R : LogicRealization.{0, 0}) :
    (UniversalForcing.arithmeticOf canonicalCategoricalRealization).peano.carrier
      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
  ArithmeticOf.equivOfInitial
    (UniversalForcing.arithmeticOf canonicalCategoricalRealization)
    (UniversalForcing.arithmeticOf R)

What this page does not claim

This module does not rebuild category theory or provide a full category instance. The invariance theorem does not state that all realizations are identical, only that their carriers are equivalent. The module does not derive the natural numbers from nothing; it builds them from a prior logical construction.

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