Peano arithmetic

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-22.
Last modified on 2024-10-16.

module elementary-number-theory.peano-arithmetic where

Imports

open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negated-equality
open import foundation.propositions
open import foundation.universe-levels

Axioms

We state the Peano axioms^¶ in type theory using the identity type as equality, and prove that they hold for the natural numbers ℕ.

Peano’s 1st axiom

There is an element zero of the natural numbers.

peano-axiom-1 : {l : Level} → UU l → UU l
peano-axiom-1 N = N

peano-1-ℕ : peano-axiom-1 ℕ
peano-1-ℕ = zero-ℕ

Peano’s 2nd axiom

The identity relation on the natural numbers is reflexive. I.e. for every natural number x, it is true that x ＝ x.

peano-axiom-2 : {l : Level} → UU l → UU l
peano-axiom-2 N = (x : N) → x ＝ x

peano-2-ℕ : peano-axiom-2 ℕ
peano-2-ℕ x = refl

Peano’s 3rd axiom

The identity relation on the natural numbers is symmetric. I.e. if x ＝ y, then y ＝ x.

peano-axiom-3 : {l : Level} → UU l → UU l
peano-axiom-3 N = (x y : N) → x ＝ y → y ＝ x

peano-3-ℕ : peano-axiom-3 ℕ
peano-3-ℕ x y = inv

Peano’s 4th axiom

The identity relation on the natural numbers is transitive. I.e., if y ＝ z and x ＝ y, then x ＝ z.

peano-axiom-4 : {l : Level} → UU l → UU l
peano-axiom-4 N = (x y z : N) → y ＝ z → x ＝ y → x ＝ z

peano-4-ℕ : peano-axiom-4 ℕ
peano-4-ℕ x y z = concat' x

The 5th axiom of peano’s arithmetic states that for every x and y, if x ＝ y and y is a natural number, then x is a natural number. This axiom does not make sense in type theory, as every element by definition lives in a specified type. To even pose the question of whether two elements are equal, we must already know that they are elements of the same type.

Peano’s 6th axiom

For every natural number, there is a successor natural number.

peano-axiom-6 : {l : Level} → UU l → UU l
peano-axiom-6 N = N → N

peano-6-ℕ : peano-axiom-6 ℕ
peano-6-ℕ = succ-ℕ

Peano’s 7th axiom

For two natural numbers x and y, if the successor of x is identified with the successor of y, then x is identified with y.

peano-axiom-7 : {l : Level} (N : UU l) → peano-axiom-6 N → UU l
peano-axiom-7 N succ = (x y : N) → (x ＝ y) ↔ (succ x ＝ succ y)

peano-7-ℕ : peano-axiom-7 ℕ peano-6-ℕ
pr1 (peano-7-ℕ x y) refl = refl
pr2 (peano-7-ℕ x y) = is-injective-succ-ℕ

Peano’s 8th axiom

The zero natural number may not be identified with any successor natural number.

peano-axiom-8 :
  {l : Level} (N : UU l) → peano-axiom-1 N → peano-axiom-6 N → UU l
peano-axiom-8 N zero succ = (x : N) → succ x ≠ zero

peano-8-ℕ : peano-axiom-8 ℕ peano-1-ℕ peano-6-ℕ
peano-8-ℕ = is-nonzero-succ-ℕ

Peano’s 9th axiom

The natural numbers satisfy the following propositional induction principle:

Given a predicate on the natural numbers P : N → Prop, if

P zero holds,

and

if P x holds then P (succ x) holds,

then P x holds for all natural numbers x.

peano-axiom-9 :
  {l : Level} (N : UU l) → peano-axiom-1 N → peano-axiom-6 N → UUω
peano-axiom-9 N zero succ =
  {l' : Level} (P : N → Prop l') →
  type-Prop (P zero) →
  ((x : N) → type-Prop (P x) → type-Prop (P (succ x))) →
  ((x : N) → type-Prop (P x))

peano-9-ℕ : peano-axiom-9 ℕ peano-1-ℕ peano-6-ℕ
peano-9-ℕ P = ind-ℕ {P = type-Prop ∘ P}