Foundation Universal Forcing Natural Number Object Interpret Collapses

The Boolean collapse

The natural numbers are the counting structure: a starting point and a way to step from any number to the next. The Recognition Science framework's machine-checked library of formal theorems proves that this structure is forced, not chosen, by the logic of recognition. The declaration interpret_collapses addresses a pointed objection: if the framework's arithmetic is forced, why does one of its models, the Boolean one, appear to have only two values?

The Boolean model is the sharpest possible test. Its carrier, the set of values the model can hold, contains exactly two elements, false and true. The interpretation map from the framework's counting structure to this model sends every number to one of these two values. The theorem interpret_collapses proves that this map is not injective: infinitely many distinct numbers land on the same Boolean value. In plain terms, the model's set of values collapses the counting structure down to a two-element shadow.

The theorem's real content is what does not collapse. The iteration object, the thing that does the counting, is not the set of values the model can hold. It is the framework's own counting structure, which the library proves is a Lawvere natural-number object. That is a precise categorical sense of "the natural numbers": a structure such that for any other structure with a starting point and a step function, there is exactly one way to map the counting structure into it. The library proves this property holds for the framework's counting structure, and that it is the same structure in every model, including the Boolean one. The collapse is a property of the model's carrier, not of the counting itself.

The framework's library proves that any two realizations of its arithmetic have iteration orbits that are canonically equivalent. This is the formal statement that the counting structure is unique up to unique isomorphism, in the Lawvere sense. The Boolean model is just one realization, and its two-element carrier is a test that the counting structure survives even when the model's values do not. The theorem interpret_collapses is the formal answer to the critic's worry that the framework smuggled in iteration-counting: the iteration object is the natural-number object, and it is the same in every realization.

The consequence is that the framework's arithmetic is not hostage to any particular model. The Boolean model shows that even a maximally coarse realization, one with only two values, still carries the full counting structure. The collapse is a feature of the model's representation, not a flaw in the arithmetic. What the theorem does not claim is that the Boolean model itself is the natural numbers, or that the framework derives the natural numbers from nothing. The framework's counting structure is a natural-number object, and the Boolean model is a realization of it, not a replacement for it.

/-- Even though the carrier image collapses, the iteration object is the
full `LogicNat`. Concretely: the interpretation map is not injective. -/
theorem interpret_collapses :
    ¬ Function.Injective
      (StrictLogicRealization.interpret strictBooleanRealization) := by
  intro hinj
  have h0 :
      StrictLogicRealization.interpret strictBooleanRealization LogicNat.identity =
        Nat.bodd 0 := interpret_eq_parity _
  have h2 :
      StrictLogicRealization.interpret strictBooleanRealization
        (LogicNat.step (LogicNat.step LogicNat.identity)) =
          Nat.bodd 2 := interpret_eq_parity _
  have hbodd : (Nat.bodd 0 : Bool) = Nat.bodd 2 := by decide
  have hboth :
      StrictLogicRealization.interpret strictBooleanRealization LogicNat.identity =
        StrictLogicRealization.interpret strictBooleanRealization
          (LogicNat.step (LogicNat.step LogicNat.identity)) := by
    rw [h0, h2, hbodd]
  have hne : LogicNat.identity ≠ LogicNat.step (LogicNat.step LogicNat.identity) :=
    LogicNat.zero_ne_succ _
  exact hne (hinj hboth)

/-- `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 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 Boolean model itself is the natural numbers. The framework derives the natural numbers from no premises at all. The interpretation map from the counting structure to the Boolean model is injective.

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: