Addition of Natural Numbers is Provable

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $x, y \in \N$ be natural numbers.

Then there exists formal proof of:

$\sqbrk x + \sqbrk y = \sqbrk {x + y}$

in minimal arithmetic, where $\sqbrk a$ is the unary representation of $a$.

General Form

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$

in minimal arithmetic.


Proof

By Unary Representation of Natural Number, let $\sqbrk a$ denote the term $\map s {\dots \map s 0}$, where there are $a$ applications of the successor mapping to the constant $0$.

Proceed by induction on $y$.

Base Case

Let $y = 0$.

Then $\sqbrk y = 0$.

The following is a formal proof:




By the tableau method of natural deduction:

$\sqbrk x + 0 = \sqbrk x$
Line Pool Formula Rule Depends upon Notes
1 $\forall a: a + 0 = a$ Axiom $\text M 3$
2 $\sqbrk x + 0 = \sqbrk x$ Universal Instantiation 1


But $x + 0 = x$.

Therefore, $\sqbrk {x + 0} = \sqbrk x$.

Thus, the proof above is a formal proof of $\sqbrk x + 0 = \sqbrk {x + 0}$.

$\Box$

Induction Step

Let there exist a formal proof of $\sqbrk x + \sqbrk y = \sqbrk {x + y}$.

Then, the following is a formal proof:


By the tableau method of natural deduction:

$\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk {x + y} } $
Line Pool Formula Rule Depends upon Notes
1 $\sqbrk x + \sqbrk y = \sqbrk {x + y}$ Theorem Introduction (None) Induction hypothesis
2 $\forall a, b: a = b \implies \map s a = \map s b$ Theorem Introduction (None) Substitution Property of Equality
3 $\sqbrk x + \sqbrk y = \sqbrk {x + y} \implies \map s {\sqbrk x + \sqbrk y} = \map s {\sqbrk {x + y} }$ Universal Instantiation 2
4 $\map s {\sqbrk x + \sqbrk y} = \map s {\sqbrk {x + y} }$ Modus Ponendo Ponens 3, 1
5 $\forall a, b: a + \map s b = \map s {a + b}$ Axiom $\text M 4$
6 $\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk x + \sqbrk y}$ Universal Instantiation 7
7 $\paren {\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk x + \sqbrk y} } \land \paren {\map s {\sqbrk x + \sqbrk y} = \map s {\sqbrk {x + y} } }$ Rule of Conjunction 6, 4
8 $\forall a,b,c: \paren {a = b} \land \paren {b = c} \implies a = c$ Theorem Introduction (None) Equality is Transitive
9 $\paren {\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk x + \sqbrk y} } \land \paren {\map s {\sqbrk x + \sqbrk y} = \map s {\sqbrk {x + y} } } \implies \sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk {x + y} }$ Universal Instantiation 8
10 $\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk {x + y} }$ Modus Ponendo Ponens 9, 7


Therefore, there exists a formal proof of $\sqbrk x + \map s {\sqbrk y} = \map s {\sqbrk {x + y} }$.

But as:

$\sqbrk a$

consists of $a$ applications of the successor mapping to the constant $0$, it follows that:

$\map s {\sqbrk y} = \sqbrk {\map s y}$

consists of $a + 1 = \map s a$ applications of $s$ to $0$.

But that is the unary representation of $\map s a$.

Therefore:

$\map s {\sqbrk y} = \sqbrk {\map s y}$

and

$\map s {\sqbrk {x + y} } = \sqbrk {\map s {x + y} }$

By the definition of addition, $x + \map s y = \map s {x + y}$.

Thus:

$\sqbrk {\map s {x + y} } = \sqbrk {x + \map s y}$

It follows that the proof above is also a proof of:

$\sqbrk x + \sqbrk {\map s y} = \sqbrk {x + \map s y}$

$\Box$


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

As $x$ was arbitrary, there exists such a formal proof for every $x, y \in \N$.

$\blacksquare$