Encyclopedia Foundation Foundation Integers From Logic

ARTICLE 4 claims 3 theorems 1 model

Foundation Integers From Logic

Integers are built from pairs of natural numbers, and this construction is proven unique.

Verify this page

Integers from logic

Integers are the numbers that include negatives: ..., -2, -1, 0, 1, 2, ... . A standard way to build them from natural numbers (0, 1, 2, ...) is to define an integer as a pair of naturals, (a, b), which represents the difference a - b. The pair (3, 1) and the pair (4, 2) both represent the integer 2, so the construction uses an equivalence relation: (a, b) ~ (c, d) iff a + d = c + b. This is called the Grothendieck equivalence, named after the mathematician Alexander Grothendieck, who used similar constructions widely in algebraic geometry.

The IntegersFromLogic construction in the Recognition Science framework's machine-checked library of formal theorems builds this construction inside the framework's own logic. It defines a type LogicInt as the set of all such pairs under the equivalence relation. It then provides the usual operations: zero, one, addition, negation, and multiplication. Each operation is defined on pairs and respects the equivalence, so the resulting structure behaves exactly like the integers.

The construction is proven correct and unique. A function toInt maps each LogicInt to the standard integer it represents, and the theorem fromInt_toInt shows this map is a bijection: every LogicInt corresponds to exactly one standard integer, and vice versa. The order relations less-than and less-than-or-equal are also defined and proven to match the standard order on integers. The theorem le_relation_unique shows that the less-than-or-equal relation on LogicInt is the unique relation that agrees with the standard integer order under this map.

The construction also proves the algebraic laws that make LogicInt a proper number system. Addition and multiplication are commutative, zero is the additive identity, one is the multiplicative identity, and every element has an additive inverse, so -a + a = 0. The theorem mul_eq_zero proves the zero-product property: a product is zero if and only if one of its factors is zero. These laws are all verified by reducing to the corresponding laws for standard integers, using the bijection.

In Recognition Science, this construction is part of the foundation: it shows that the framework's logic can construct the integers from its own natural numbers, without assuming them as primitive. The framework proves the integers exist and behave correctly within its own system. The uniqueness results mean there is no ambiguity in how the integers are represented, which matters for the framework's later derivations. The construction is a standard mathematical technique, and the contribution is to verify it formally inside the framework's logic.

MODEL intRel · LogicInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean
intRel · IndisputableMonolith/Foundation/IntegersFromLogic.lean:39 
/-- The Grothendieck equivalence relation on pairs of `LogicNat`:
`(a, b) ~ (c, d)` iff `a + d = c + b`. The pair `(a, b)` represents
the formal difference `a - b`. -/
def intRel : (LogicNat × LogicNat) → (LogicNat × LogicNat) → Prop :=
  fun p q => p.1 + q.2 = q.1 + p.2
LogicInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean:75 
/-- `LogicInt` is the Grothendieck completion of `LogicNat` under
addition. -/
def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))
THEOREM fromInt_toInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean
fromInt_toInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean:219 
theorem fromInt_toInt : ∀ z : LogicInt, fromInt (toInt z) = z := by
  intro z
  induction z using Quotient.inductionOn with
  | h p =>
    rcases p with ⟨a, b⟩
    show fromInt (toInt (mk a b)) = mk a b
    rw [toInt_mk]
    -- (toNat a : Int) - toNat b. Case on sign.
    by_cases h : toNat b ≤ toNat a
    · -- Non-negative case
      have hge : (0 : Int) ≤ (toNat a : Int) - toNat b := by
        have : (toNat b : Int) ≤ toNat a := by exact_mod_cast h
        linarith
      obtain ⟨k, hk⟩ := Int.eq_ofNat_of_zero_le hge
      rw [hk]
      show fromInt (Int.ofNat k) = mk a b
      show mk (LogicNat.fromNat k) LogicNat.zero = mk a b
      apply sound
      -- LogicNat.fromNat k + b = a + 0 = a in LogicNat.
      -- We have: (toNat a : Int) - toNat b = k as Int, so toNat a = toNat b + k in Nat.
      have hknat : (k : Int) = (toNat a : Int) - toNat b := hk.symm
      have hknat' : toNat a = toNat b + k := by
        have : (toNat a : Int) = toNat b + k := by linarith
        exact_mod_cast this
      show LogicNat.fromNat k + b = a + LogicNat.zero
      rw [LogicNat.add_zero]
      have hcast := congrArg fromNat hknat'
      rw [LogicNat.fromNat_toNat] at hcast
      -- hcast : a = fromNat (toNat b + k)
      -- We need: fromNat k + b = a
      have : LogicNat.fromNat (toNat b + k) = LogicNat.fromNat (toNat b) + LogicNat.fromNat k := by
        -- fromNat is an additive homomorphism. Prove directly.
        have hh : toNat (LogicNat.fromNat (toNat b) + LogicNat.fromNat k)
                  = toNat b + k := by
          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
        have := congrArg LogicNat.fromNat hh
        rw [LogicNat.fromNat_toNat] at this
        exact this.symm
      rw [hcast, this, LogicNat.fromNat_toNat, LogicNat.add_comm]
    · -- Negative case
      push_neg at h
      have hlt : (toNat a : Int) < toNat b := by exact_mod_cast h
      have hltz : (toNat a : Int) - toNat b < 0 := by linarith
      have hsub_pos : 0 < toNat b - toNat a := Nat.sub_pos_of_lt h
      -- (toNat a : Int) - toNat b = -(toNat b - toNat a) and is Int.negSucc of (toNat b - toNat a - 1).
      set m := toNat b - toNat a - 1 with hm_def
      have hsucc : Nat.succ m = toNat b - toNat a := by
        rw [hm_def]
        omega
      have heq : (toNat a : Int) - toNat b = Int.negSucc m := by
        rw [Int.negSucc_eq]
        have h1 : ((Nat.succ m : Int)) = (toNat b - toNat a : Int) := by
          rw [hsucc]
          push_cast
          omega
        push_cast at h1
        linarith
      rw [heq]
      show fromInt (Int.negSucc m) = mk a b
      show mk LogicNat.zero (LogicNat.fromNat (Nat.succ m)) = mk a b
      apply sound
      -- Want: 0 + b = a + fromNat (succ m), i.e. b = a + fromNat (succ m).
      show LogicNat.zero + b = a + LogicNat.fromNat (Nat.succ m)
      rw [LogicNat.zero_add]
      -- toNat b = toNat a + Nat.succ m by hsucc.
      have hbnat : toNat b = toNat a + Nat.succ m := by
        rw [hsucc]; omega
      have hcast := congrArg LogicNat.fromNat hbnat
      rw [LogicNat.fromNat_toNat] at hcast
      have hadd_morph : LogicNat.fromNat (toNat a + Nat.succ m)
                        = LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m) := by
        have hh : toNat (LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m))
                  = toNat a + Nat.succ m := by
          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
        have := congrArg LogicNat.fromNat hh
        rw [LogicNat.fromNat_toNat] at this
        exact this.symm
      rw [hcast, hadd_morph, LogicNat.fromNat_toNat]
THEOREM le_relation_unique · IndisputableMonolith/Foundation/IntegersFromLogic.lean
le_relation_unique · IndisputableMonolith/Foundation/IntegersFromLogic.lean:393 
/-- Any non-strict relation with the required transport law is the canonical
pulled-back relation. -/
theorem le_relation_unique
    (r : LogicInt → LogicInt → Prop)
    (h : ∀ a b, r a b ↔ toInt a ≤ toInt b) :
    r = le := by
  funext a b
  apply propext
  exact h a b
THEOREM mul_eq_zero · IndisputableMonolith/Foundation/IntegersFromLogic.lean
mul_eq_zero · IndisputableMonolith/Foundation/IntegersFromLogic.lean:490 
/-- `LogicInt` has no zero divisors: from `a * b = 0`, either `a = 0`
or `b = 0`. Forced by the ring isomorphism with `Int`. -/
theorem mul_eq_zero {a b : LogicInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
  constructor
  · intro h
    have hint : toInt a * toInt b = 0 := by
      rw [← toInt_mul]
      have := congrArg toInt h
      rwa [toInt_zero] at this
    rcases Int.mul_eq_zero.mp hint with ha | hb
    · left
      rw [eq_iff_toInt_eq, toInt_zero]; exact ha
    · right
      rw [eq_iff_toInt_eq, toInt_zero]; exact hb
  · rintro (ha | hb)
    · rw [ha, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
    · rw [hb, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring

What this page does not claim

This construction does not construct the real numbers or complex numbers. The uniqueness of the order relation does not imply uniqueness of the entire integer structure. The framework does not claim that integers are physically real; it claims they can be constructed within its logic.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND