Peano arithmetic
Content created by Fredrik Bakke and Egbert Rijke.
Created on 2023-10-22.
Last modified on 2024-10-09.
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
Peano’s 5th axiom
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 thenP (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}
External links
- Peano axioms at Mathswitch
- Peano arithmetic at Lab
- Peano axioms at Britannica
- Peano axioms at Wikipedia
- Peano’s Axioms at Wolfram Mathworld
Recent changes
- 2024-10-09. Fredrik Bakke. Idea text
set-theory
(#1189). - 2023-11-09. Fredrik Bakke. Typeset
nlab
as$n$Lab
(#911). - 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).
- 2023-10-22. Fredrik Bakke and Egbert Rijke. Peano arithmetic (#876).