Foundation Universal Forcing Natural Number Object Forced Arithmetic Is Nno

The forced counting structure

The natural numbers are the counting numbers 0, 1, 2, 3, and so on. In category theory, a branch of mathematics that studies structures and the maps between them, there is a precise way to say what counting is without already having the numbers. A natural-number object is a triple (N, z, s) where N is a set, z is a chosen starting point, and s is a successor map, such that for any other set X with a starting point x and a map f from X to itself, there is exactly one map h from N to X that sends z to x and commutes with s and f. This property, called the Lawvere characterization after the mathematician F. William Lawvere who formulated it in the 1960s, captures the idea of primitive recursion: it is what allows definitions like addition and multiplication to be built by repeated application.

The framework's library of formal theorems contains a declaration named forcedArithmetic_isNNO. It states that for every realization of the framework's logic, the forced arithmetic, which is the iteration orbit of the realization, satisfies the Lawvere natural-number object property. In plainer language: no matter how the framework's logic is realized, the structure that counts iteration steps is always the natural numbers. The proof works by transporting the natural-number object structure from a specific object called LogicNat through the realization's certified orbit equivalence. The declaration is a theorem in the machine-checked library, meaning it has been verified by a computer proof assistant.

The importance of this result is that it answers a specific criticism. A skeptic might say that the framework has not really derived the natural numbers, but has merely assumed iteration counting somewhere in its foundations. The declaration shows that the iteration object, the thing that counts steps, is itself a natural-number object in the Lawvere sense. This is true even in the most extreme case: the strict Boolean realization, whose carrier set has only two elements, true and false. In that realization, the interpretation map collapses infinitely many iteration steps onto two values, the parity of the count. But the iteration object itself does not collapse; it remains the full natural-number object, canonically equivalent to the one in any other realization.

What the declaration does not claim is equally important. It does not claim that the framework derives the natural numbers from nothing, or that it proves the consistency of arithmetic. The natural-number object property is a structural characterization, not a construction of numbers from scratch. The declaration also does not claim that the Boolean realization's carrier set is the natural numbers; it explicitly shows that the carrier collapses to two elements. The claim is about the iteration object, which is the natural-number object, and about its uniqueness up to canonical isomorphism across all realizations. This uniqueness is what the framework calls universal forcing at the natural-number object level: every realization carries the same counting structure.

/-- The forced arithmetic of every realization is canonically equivalent to
`LogicNat`. This is the Universal Forcing statement at the natural-number
object level: every Law-of-Logic realization carries the same NNO. -/
noncomputable def realizationOrbit_equiv_logicNat (R : LogicRealization.{0, 0}) :
    R.Orbit ≃ LogicNat :=
  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) logicNat_isNNO

/-- The Lawvere universality statement: any two realizations have iteration
orbits that satisfy the natural-number-object property, hence are
canonically equivalent. -/
noncomputable def universal_forcing_via_NNO
    (R S : LogicRealization.{0, 0}) : R.Orbit ≃ S.Orbit :=
  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) (realizationOrbit_isNNO S)

/-- The Boolean strict-realization interpretation is the parity map.

This is the formal statement that the iteration count survives even when
the orbit-as-set collapses to `{false, true}`. -/
theorem interpret_eq_parity (n : LogicNat) :
    StrictLogicRealization.interpret strictBooleanRealization n =
      Nat.bodd (LogicNat.toNat n) := by
  induction n with
  | identity => rfl
  | step n ih =>
      show xorBool true (StrictLogicRealization.interpret strictBooleanRealization n) =
        Nat.bodd (Nat.succ (LogicNat.toNat n))
      rw [xorBool_true, ih, Nat.bodd_succ]

What this page does not claim

The declaration does not derive the natural numbers from nothing; it characterizes them structurally via the Lawvere property. The declaration does not claim the Boolean realization's carrier set is the natural numbers; it explicitly shows the carrier collapses to two elements. The declaration does not prove the consistency of arithmetic or any foundational axiom system.

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/UniversalForcing/NaturalNumberObject.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: