---
tag: 0TBYMWPWWB
kind: statement
role: axiom
name: The successor function is injective
msc: [03F30]
uses: [0832XVR512, 0QFT7Z76N5]
sources:
  - url: https://en.wikipedia.org/wiki/Peano_axioms
    locator: Historical second-order formulation
---

## Statement

Let $S \colon \mathbb{N} \to \mathbb{N}$ be the [[successor function|0832XVR512]] of the natural numbers.
For all natural numbers $m$ and $n$, if $S(m) = S(n)$, then $m = n$.

## Remarks

This is one of the [[Peano axioms|0QFT7Z76N5]]. In a construction of $\mathbb{N}$, for example in set theory, it is a theorem.
An equivalent form is: if $m \neq n$, then $m + 1 \neq n + 1$.

## Explanations

### L1 human

Two different numbers never have the same next number.
If you know the number after $n$, then you know $n$.