Foundation Universal Forcing Natural Number Object Is Natural Number Object

The forced counting structure

A natural-number object is a categorical way to describe the counting numbers without assuming they already exist. It is a triple (N, z, s): a collection N, a starting element z, and a function s that moves from one element to the next. The defining property, due to the mathematician F. William Lawvere in the 1960s, is that for any other collection X with a starting point x and a function f, there is exactly one way to define a map from N to X that sends z to x and commutes with the step functions. This universal property is what makes the structure behave like the natural numbers: it is the initial pointed endomap algebra, the most basic example of a set with a distinguished point and a self-map.

The framework's machine-checked library of formal theorems proves that its own constructed counting structure, called LogicNat, satisfies this Lawvere property. The proof is direct: it defines the required recursor, shows it behaves correctly on the starting element and under the step function, and demonstrates that any other map with the same behavior must equal it. The library then shows that every realization of the framework's logic, no matter how its carrier set is chosen, produces an iteration orbit that is also a natural-number object. Because any two natural-number objects are canonically isomorphic, this means every realization carries the same counting structure, equivalent to LogicNat itself.

The sharpest test comes from a realization whose carrier set has only two elements, the booleans. Its interpretation map sends infinitely many iteration steps onto just two values, so the map is not injective. Yet the iteration object itself, the thing that counts the steps, remains the full LogicNat. The library proves this by showing the boolean interpretation is exactly the parity map, which distinguishes even and odd but nothing finer. This addresses a critic's worry that the framework smuggled in iteration counting: the iteration object is the natural-number object in the Lawvere sense, and it is the same in every realization, including the discrete boolean one.

Within the framework, this result means the natural numbers are not an assumption but a consequence of the logic itself. The declaration IsNaturalNumberObject is the formal statement of that consequence: it packages the recursor, its zero and step laws, and uniqueness into a single structure. What it does not claim is that the framework derives the natural numbers from nothing, nor that it proves the existence of an infinite set in any absolute sense. The theorem is about the structure of counting within the framework's own logic, not about the metaphysical status of numbers outside it.

/-- `LogicNat` with `identity` and `step` is a Lawvere natural-number object. -/
def logicNat_isNNO :
    IsNaturalNumberObject (N := LogicNat) LogicNat.identity LogicNat.step where
  recursor := fun {X} x f => ArithmeticOf.logicNatFold ⟨X, x, f⟩
  recursor_zero := fun _ _ => rfl
  recursor_step := fun _ _ _ => rfl
  recursor_unique := by
    intro X x f h hz hs n
    induction n with
    | identity => exact hz
    | step n ih =>
        calc
          h (LogicNat.step n) = f (h n) := hs n
          _ = f (ArithmeticOf.logicNatFold ⟨X, x, f⟩ n) := by rw [ih]
          _ = ArithmeticOf.logicNatFold ⟨X, x, f⟩ (LogicNat.step n) := rfl

/-- 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 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 framework derives the natural numbers from nothing or proves their existence absolutely. The natural-number object theorem establishes the consistency of the framework's logic. The boolean realization's iteration object is the same as its carrier set.

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: