Unary Representation of Natural Number

Theorem

Let $x \in \N$ be a natural number.

Then:

$x = \map s {\map s {\dots \map s 0} }$

where there are $x$ applications of the successor mapping to the constant $0$.

Proof

We shall proceed by induction.

Base Case

When $x = 0$, we have:

$0 = 0$

which follows from Equality is Reflexive.

But that is zero applications of the successor mapping to the constant $0$.

$\Box$

Induction Step

Let $x \in \N$ satisfy the theorem.

Then:

$x = \map s {\map s {\dots \map s 0} }$

where there are $x$ applications of the successor mapping.

Denote the term as $\phi$.

But by Substitution Property of Equality:

$\map s x = \map s \phi$

But $\map s \phi$ consists of $x + 1 = \map s x$ applications of the successor mapping to the constant $0$.

$\Box$

Thus, by Principle of Mathematical Induction, the theorem holds for every $x \in \N$.

$\blacksquare$