`succ`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 80 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  77@[simp] def zero : LogicNat := .identity
  78
  79/-- Successor is one more application of the generator. -/
  80@[simp] def succ (n : LogicNat) : LogicNat := .step n
  81
  82/-! ## 3. Peano Axioms as Theorems
  83
  84Each axiom is a theorem of the inductive structure. None is posited.
  85-/
  86
  87/-- **Peano P1 (zero is not a successor)**: the identity is
  88distinguishable from any iterate of the generator. -/
  89theorem zero_ne_succ (n : LogicNat) : zero ≠ succ n := by
  90  intro h; cases h
  91
  92/-- **Peano P1, contrapositive**: every successor differs from zero. -/
  93theorem succ_ne_zero (n : LogicNat) : succ n ≠ zero := by
  94  intro h; cases h
  95
  96/-- **Peano P2 (successor injectivity)**: forced by the constructor
  97disjointness of the inductive type, which itself reflects the
  98injectivity of multiplication by the generator on the orbit. -/
  99theorem succ_injective : Function.Injective succ := by
 100  intro a b h
 101  cases h
 102  rfl
 103
 104/-- **Peano P3 (induction)**: any property closed under successor and
 105holding at zero holds for every `LogicNat`. -/
 106theorem induction
 107    {motive : LogicNat → Prop}
 108    (h0 : motive zero)
 109    (hs : ∀ n, motive n → motive (succ n)) :
 110    ∀ n, motive n := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.