# 1+1 = 2

## Theorem

Define $0$ as the unique element in the set $P \setminus \map s P$, where:

$P$ is the Peano Structure
$\map s P$ is the image of the mapping $s$ defined in Peano structure
$\setminus$ denotes the set difference.

Then:

$1 + 1 = 2$

where:

$1 := \map s 0$
$2 := \map s 1 = \map s {\map s 0}$
$+$ denotes addition
$=$ denotes equality
$\map s n$ denotes the successor mapping.

## Proof 1

$1$ is defined by hypothesis as $\map s 0$ and $2$ as $\map s {\map s 0}$.

Hence the statement to be proven becomes:

$\map s 0 + \map s 0 = \map s {\map s 0}$

Thus:

 $\ds \forall m, n \in P: \,$ $\ds m + \map s n$ $=$ $\ds \map s {m + n}$ Definition of Addition in Peano Structure $\ds \leadsto \ \$ $\ds \forall m \in P: \,$ $\ds m + \map s 0$ $=$ $\ds \map s {m + 0}$ as $0 \in P$ $\text {(1)}: \quad$ $\ds \leadsto \ \$ $\ds \map s 0 + \map s 0$ $=$ $\ds \map s {\map s 0 + 0}$ as $\map s 0 \in P$ Then: $\ds \forall m \in P: \,$ $\ds m + 0$ $=$ $\ds m$ Definition of Addition in Peano Structure $\ds \leadsto \ \$ $\ds \map s 0 + 0$ $=$ $\ds \map s 0$ as $\map s 0 \in P$ $\ds \map s {\map s 0 + 0}$ $=$ $\ds \map s {\map s 0}$ taking the successor on both sides of $(2)$ $\ds \leadsto \ \$ $\ds \map s 0 + \map s 0$ $=$ $\ds \map s {\map s 0}$ substituting for $\map s {\map s 0 + 0}$ from $(1)$

$\blacksquare$

## Proof 2

Defining $1$ as $\map s 0$ and $2$ as $\map s {\map s 0}$, the statement to be proven becomes:

$\map s 0 + \map s 0 = \map s {\map s 0}$

By the definition of addition:

$\forall m \in P: \forall n \in P: m + \map s n = \map s {m + n}$

Letting $m = \map s 0$ and $n = 0$:

 $\text {(1)}: \quad$ $\ds \map s 0 + \map s 0$ $=$ $\ds \map s {\map s 0 + 0}$

By the definition of addition:

$\forall m: m + 0 = m$

Letting $m = \map s 0$:

$\map s 0 + 0 = \map s 0$

Taking the successor of both sides:

 $\text {(2)}: \quad$ $\ds \map s {\map s 0 + 0}$ $=$ $\ds \map s {\map s 0}$

Applying Equality is Transitive to $(1)$ and $(2)$ we have:

$\map s 0 + \map s 0 = \map s {\map s 0}$

Hence the result.

$\blacksquare$