Foundation Arithmetic From Logic

Arithmetic from logic

In mathematics, the natural numbers are usually introduced as a starting point: 0, 1, 2, 3, and so on, built by repeatedly adding one. Recognition Science asks a different question. Instead of assuming numbers exist, it asks what minimal structure a comparison operator must have, and whether that structure alone forces something that looks like arithmetic. The answer, proved in a machine-checked library of formal theorems, is that it does. The natural numbers are not a primitive assumption but a consequence of the logic of comparison.

The starting point is a ledger, a discrete record of events, where each event has a cost of recognition. The framework proves that any cost function satisfying five plain conditions must take a specific form, and from that form a non-trivial generator γ ≠ 1 emerges. This generator is a positive real number, not equal to 1, that produces an orbit under repeated multiplication: 1, γ, γ², γ³, and so on. This orbit, together with the identity element 1, has exactly two ways to build new elements: be at the identity, or take one more step. That two-constructor structure is precisely the structure of the natural numbers.

The module ArithmeticFromLogic formalizes this insight. It defines an inductive type called LogicNat with two constructors: identity and step. The identity represents the zero-cost element, the multiplicative identity in the orbit. The step constructor represents one more iteration of the generator. This mirrors the orbit {1, γ, γ², γ³, ...} as the smallest subset of the positive reals closed under multiplication by γ and containing 1. The definition makes no reference to base 10, base 2, or any positional system. The only primitives are the identity element and the step operation.

From this minimal starting point, the module proves the standard properties of arithmetic. It defines addition and multiplication recursively, following the usual pattern: adding zero leaves a number unchanged, and adding a successor is the successor of the sum. It proves that zero is not a successor, that the successor function is injective, and that the order relation works as expected. These are the Peano axioms, derived not from a choice of axioms but from the forced structure of comparison.

The result is that arithmetic is not a human invention layered on top of reality. Within the framework, it is the inevitable structure of any non-trivial comparison operator. The natural numbers are not a convention; they are what the logic of recognition forces. This does not mean the framework claims to derive all of mathematics from nothing. It starts with the laws of logic themselves and shows that the natural numbers are a necessary consequence of those laws.

/-- The natural numbers as forced by the Law of Logic.

`identity` represents the zero-cost element (the multiplicative
identity in the orbit). `step` represents one more iteration of the
generator. The two-constructor structure mirrors the orbit
{1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under
multiplication by γ and containing 1. -/
inductive LogicNat : Type
  | identity : LogicNat
  | step     : LogicNat → LogicNat
  deriving DecidableEq, Repr

/-- **Peano P1, contrapositive**: every successor differs from zero. -/
theorem succ_ne_zero (n : LogicNat) : succ n ≠ zero := by
  intro h; cases h

/-- **Peano P2 (successor injectivity)**: forced by the constructor
disjointness of the inductive type, which itself reflects the
injectivity of multiplication by the generator on the orbit. -/
theorem succ_injective : Function.Injective succ := by
  intro a b h
  cases h
  rfl

/-- The natural numbers as forced by the Law of Logic.

`identity` represents the zero-cost element (the multiplicative
identity in the orbit). `step` represents one more iteration of the
generator. The two-constructor structure mirrors the orbit
{1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under
multiplication by γ and containing 1. -/
inductive LogicNat : Type
  | identity : LogicNat
  | step     : LogicNat → LogicNat
  deriving DecidableEq, Repr

What this page does not claim

This module does not derive the full structure of arithmetic from no assumptions at all, only from the laws of logic. It does not claim that the natural numbers are the only possible structure, only that they are forced by a non-trivial comparison operator. The module does not address how the natural numbers relate to other number systems like the integers or reals.

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