Categoricity

Difficulty: moderate — 2 definitions, 0 abbreviations, 4 lemmas, 1 theorems, 0 examples.

definition lemma theorem
legend

Peano’s postulate pins the model down completely: any model satisfying it is the natural numbers, relabelled.

The argument is counting. In such a model the successor lies strictly above, since the wrap-around clause would give a zero a predecessor. So counting from the zero climbs strictly, and each natural number names a different element. Counting also reaches everything, since an element is either a zero, or the successor of something below it, and descending that way ends after finitely many steps. Strictly climbing and reaching everything together make the count an order isomorphism, so there are no models beyond the standard one.

Under Peano’s postulate the successor lies strictly above, since the wrap-around clause would give a zero a predecessor.

theorem Structure.Arithmetic.lt_succ.{u_1} {U : Type u_1} [Structure.Arithmetic.Peano U] (a : U) :
  a < Structure.Arithmetic.succ a
Show details 
fun {U} [Structure.Arithmetic.Peano U] a =>
  Or.casesOn (Structure.Arithmetic.S_succ a) (fun h => And.casesOn h fun h right => h) fun h =>
    And.casesOn h fun hm hz =>
      absurd ⟨hz, Or.inr ⟨hm, hz⟩⟩
        (Structure.Arithmetic.Peano.peano a (Structure.Arithmetic.succ a))

Complexity: 1533 (size of the value term)

Dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.succ

Proof dependencies: Structure.Arithmetic.M, Structure.Arithmetic.S, Structure.Arithmetic.S_succ, Structure.Arithmetic.Z

Lean core dependencies: And, absurd

Used by: Structure.Arithmetic.count_strictMono

Counting from the zero: \(n\) names the element reached by taking the successor \(n\) times.

def Structure.Arithmetic.count.{u_2} (U : Type u_2) [Structure.Arithmetic.Peano U] : ℕ → U
Show details 
| Structure.Arithmetic.count U n = Structure.Arithmetic.succ^[n] (Structure.Arithmetic.zero U)

Complexity: 33 (size of the value term)

Outer dependencies: Structure.Arithmetic.Peano

Inner dependencies: Structure.Arithmetic.succ, Structure.Arithmetic.zero

Mathlib dependencies: Nat.iterate

Lean core dependencies: Nat

Used by: Structure.Arithmetic.count_strictMono, Structure.Arithmetic.count_succ, Structure.Arithmetic.count_surjective, Structure.Arithmetic.peanoOrderIso

theorem Structure.Arithmetic.count_succ.{u_1} {U : Type u_1} [Structure.Arithmetic.Peano U] (n : ℕ) :
  Structure.Arithmetic.count U (n + 1) = Structure.Arithmetic.succ (Structure.Arithmetic.count U n)
Show details 
fun {U} [Structure.Arithmetic.Peano U] n =>
  Function.iterate_succ_apply' Structure.Arithmetic.succ n (Structure.Arithmetic.zero U)

Complexity: 33 (size of the value term)

Dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.count, Structure.Arithmetic.succ

Proof dependencies: Structure.Arithmetic.zero

Mathlib dependencies: Function.iterate_succ_apply'

Lean core dependencies: Eq, Nat

Used by: Structure.Arithmetic.count_strictMono, Structure.Arithmetic.count_surjective

Counting climbs strictly, so each natural number names a different element.

theorem Structure.Arithmetic.count_strictMono.{u_1} {U : Type u_1} [Structure.Arithmetic.Peano U] :
  StrictMono (Structure.Arithmetic.count U)
Show details 
fun {U} [Structure.Arithmetic.Peano U] =>
  strictMono_nat_of_lt_succ fun n =>
    Eq.mpr
      (id
        (congrArg (fun _a => Structure.Arithmetic.count U n < _a)
          (Structure.Arithmetic.count_succ n)))
      (Structure.Arithmetic.lt_succ (Structure.Arithmetic.count U n))

Complexity: 467 (size of the value term)

Dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.count

Proof dependencies: Structure.Arithmetic.count_succ, Structure.Arithmetic.lt_succ, Structure.Arithmetic.succ

Mathlib dependencies: StrictMono, strictMono_nat_of_lt_succ

Lean core dependencies: Eq, Eq.mpr, Nat, congrArg, id

Used by: Structure.Arithmetic.peanoOrderIso

theorem Structure.Arithmetic.eq_succ_of_S.{u_1} {U : Type u_1} [Structure.Arithmetic.Peano U] {u a : U}
  (h : Structure.Arithmetic.S u a) : a = Structure.Arithmetic.succ u
Show details 
fun {U} [Structure.Arithmetic.Peano U] {u a} h => Structure.Arithmetic.eq_the h

Complexity: 55 (size of the value term)

Dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.S, Structure.Arithmetic.succ

Proof dependencies: Structure.Arithmetic.eq_the, Structure.Arithmetic.instDefS

Lean core dependencies: Eq

Used by: Structure.Arithmetic.count_surjective

Counting reaches everything: an element is either a zero, or the successor of something below it, and descending that way ends after finitely many steps.

theorem Structure.Arithmetic.count_surjective.{u_1} {U : Type u_1} [Structure.Arithmetic.Peano U] :
  Function.Surjective (Structure.Arithmetic.count U)
Show details 
fun {U} [Structure.Arithmetic.Peano U] a =>
  WellFounded.induction Structure.Arithmetic.lt_wf a fun a ih =>
    if ha : Structure.Arithmetic.Z a then
      Exists.intro 0
        (le_antisymm (Structure.Arithmetic.Z_zero a) (ha (Structure.Arithmetic.count U 0)))
    else
      Exists.casesOn (Structure.Arithmetic.exists_S_of_not_Z ha) fun u hu =>
        Exists.casesOn (ih u (Structure.Arithmetic.S_lt ha hu)) fun n h =>
          Eq.ndrec (motive := fun u =>
            Structure.Arithmetic.S u a → ∃ n, Structure.Arithmetic.count U n = a)
            (fun hu =>
              Exists.intro (n + 1)
                (Eq.mpr (id (congrArg (fun _a => _a = a) (Structure.Arithmetic.count_succ n)))
                  (Eq.mpr
                    (id
                      (congrArg (fun _a => _a = a)
                        (Eq.symm (Structure.Arithmetic.eq_succ_of_S hu))))
                    (Eq.refl a))))
            h hu

Complexity: 1009 (size of the value term)

Dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.count

Proof dependencies: Structure.Arithmetic.S, Structure.Arithmetic.S_lt, Structure.Arithmetic.Z, Structure.Arithmetic.Z_zero, Structure.Arithmetic.count_succ, Structure.Arithmetic.eq_succ_of_S, Structure.Arithmetic.exists_S_of_not_Z, Structure.Arithmetic.lt_wf, Structure.Arithmetic.succ

Mathlib dependencies: le_antisymm

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Exists, Function.Surjective, Nat, Not, WellFounded.induction, congrArg, dite, id

Used by: Structure.Arithmetic.peanoOrderIso

Categoricity: a model satisfying Peano’s postulate is the natural numbers, order and all.

categoricity
def Structure.Arithmetic.peanoOrderIso.{u_1} {U : Type u_1} [Structure.Arithmetic.Peano U] : ℕ ≃o U
Show details 
| Structure.Arithmetic.peanoOrderIso =
  StrictMono.orderIsoOfSurjective (Structure.Arithmetic.count U) ⋯ ⋯

Complexity: 61 (size of the value term)

Outer dependencies: Structure.Arithmetic.Peano

Inner dependencies: Structure.Arithmetic.count, Structure.Arithmetic.count_strictMono, Structure.Arithmetic.count_surjective

Mathlib dependencies: OrderIso, StrictMono.orderIsoOfSurjective

Lean core dependencies: Nat

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend