Foundation Categorical Logic Realization Logic Nat Nno

The natural-number object

A natural-number object is a categorical way to say what counting is. In category theory, it packages a starting point (zero), a successor operation (adding one), and a guarantee that any other structure with the same shape is built from this one in exactly one way. This is the Lawvere formulation, named after the mathematician F. William Lawvere, who introduced it in the 1960s as a way to define the natural numbers without mentioning sets directly.

The framework's machine-checked library of formal theorems contains a declaration called logicNatNNO, which is a structure that assembles these pieces. Its object is the natural-number structure that the framework's logic already produces from its own arithmetic. Its initiality property states that this object is the initial Peano algebra: any other structure with a zero and a successor receives a unique homomorphism from it. The structure also carries a decidable equality, meaning any two of its elements can be checked for equality, and a nontriviality proof showing that the successor of zero is not equal to zero.

The declaration also connects this object to a categorical interface. It produces a one-object category interface with a zero morphism and a successor morphism, and a theorem confirms that this interface satisfies the initiality condition. A further definition, canonicalCategoricalRealization, packages the whole thing as a realization of the framework's logic. The library then proves that categorical arithmetic is invariant across realizations: the carrier of the natural-number object in the canonical realization is equivalent to the carrier in any other realization.

In Recognition Science, this declaration does not rebuild category theory. It deliberately avoids committing to a full category-theory stack, and instead names the data that a full categorical realization would eventually need to instantiate. The one-object interface is a bridge, not a finished category. The declaration establishes that the framework's logic does support a natural-number object with the right universal property, and that arithmetic built from it is the same regardless of which realization one starts from.

What this does not claim is broader. It does not claim that the framework has derived the natural numbers from nothing, nor that it has constructed a full category-theoretic foundation. It does not claim that this natural-number object is the only one, only that it is initial. And it does not claim that the categorical interface is a genuine category instance; that remains a target for future work.

/-- 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

/-- 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

/-- The categorical realization from the canonical NNO, written directly to
avoid universe inference noise from the generic `ofNNO` wrapper. -/
def canonicalCategoricalRealization : LogicRealization.{0, 0} where
  Carrier := ArithmeticFromLogic.LogicNat
  Cost := Nat
  zeroCost := inferInstance
  compare := fun x y => if x = y then 0 else 1
  zero := ArithmeticFromLogic.LogicNat.zero
  step := ArithmeticFromLogic.LogicNat.succ
  Orbit := ArithmeticFromLogic.LogicNat
  orbitZero := ArithmeticFromLogic.LogicNat.zero
  orbitStep := ArithmeticFromLogic.LogicNat.succ
  interpret := fun n => n
  interpret_zero := rfl
  interpret_step := by intro n; rfl
  orbit_no_confusion := by
    intro n h
    exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
  orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
  orbit_induction := by
    intro P h0 hs n
    exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
  orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
  orbitEquiv_zero := rfl
  orbitEquiv_step := by intro n; rfl
  identity := by intro x; simp
  nonContradiction := by
    intro x y
    by_cases h : x = y
    · subst h; simp
    · have h' : y ≠ x := by intro hyx; exact h hyx.symm
      simp [h, h']
  excludedMiddle := True
  composition := True
  actionInvariant := True
  nontrivial := by
    refine ⟨ArithmeticFromLogic.LogicNat.succ ArithmeticFromLogic.LogicNat.zero, ?_⟩
    simp

/-- 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 declaration does not construct a full category-theoretic foundation. It does not prove that the natural numbers are derived from nothing. The one-object interface is not claimed to be a genuine category instance.

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: