# Addition of Natural Numbers is Provable/General Form

## Theorem

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

Let $s^a$ denote the application of the successor mapping $a$ times.

Let $\sqbrk a$ denote $\map {s^a} 0$.

Then there exists a formal proof of:

- $\forall x: x + \sqbrk y = \map {s^y} x$

## Proof

Proceed by induction on $y$.

### Basis for the Induction

Let $y = 0$.

Then $\sqbrk y = 0$ by definition.

Then the theorem to prove is:

- $\forall x: x + 0 = x$

But that is Axiom $\text M 3$ of minimal arithmetic.

$\Box$

### Induction Hypothesis

Fix some $y \in \N$.

Suppose that there is a formal proof of:

- $\forall x: x + \sqbrk y = \map {s^y} x$

### Induction Step

The following is a formal proof:

By the tableau method of natural deduction:

Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|

1 | $\forall x: x + \sqbrk y = \map {s^y} x$ | Theorem Introduction | (None) | Induction Hypothesis | ||

2 | $x_0 + \sqbrk y = \map {s^y} {x_0}$ | Universal Instantiation | 1 | |||

3 | $\forall a,b: a + \map s b = \map s {a + b}$ | Axiom $\text M 4$ | ||||

4 | $x_0 + \map s {\sqbrk y} = \map s {x_0 + \sqbrk y}$ | Universal Instantiation | 3 | |||

5 | $\forall a, b: a = b \implies \map s a = \map s b$ | Theorem Introduction | (None) | Substitution Property of Equality | ||

6 | $x_0 + \sqbrk y = \map {s^y} {x_0} \implies \map s {x_0 + \sqbrk y} = \map s {\map {s^y} {x_0} }$ | Universal Instantiation | 5 | |||

7 | $\map s {x_0 + \sqbrk y} = \map s {\map {s^y} {x_0} }$ | Modus Ponendo Ponens | 6, 2 | |||

8 | $x_0 + \map s {\sqbrk y} = \map s {\map {s^y} {x_0} }$ | Equality is Transitive | 4, 7 | |||

9 | $\forall x: x_0 + \map s {\sqbrk y} = \map s {\map {s^y} x}$ | Universal Generalisation | 8 |

By expanding the definitions of $\sqbrk y$ and $\map {s^y} x$, the proven result is syntactically identical to:

- $\forall x: x + \sqbrk {\map s y} = \map {s^{\map s y} } x$

which was the theorem to be proven.

$\Box$

Thus, by the Principle of Mathematical Induction, there is such a formal proof for every $y \in \N$.

$\blacksquare$