**Addition of natural numbers** is the most basic arithmetic operation. Here we will define it
from Peano's axioms (see

natural number) and prove some simple properties. The natural numbers will be denoted by

**N**; zero
is taken to be a natural number.

## The Definition

The operation of **addition**, commonly written as infix operator +, is a
function of **N** x **N** -> **N**

*a + b = c*

*a* and *b* are called the addend, while *c* is being called sum.

By convention, *a*^{+} is referred as the successor of *a* as defined
in the Peano postulates.

#### The Axioms

- a+0 = a
- a+(b
^{+}) = (a+b)^{+}

The first is referred as AP1, the second as AP2.

## The Properties

- Uniqueness: (a+b) is unique
- The Law of Associativity: (a+b)+c = a+(b+c)
- The Law of Commutativity: a+b = b+a

#### Proof of Uniqueness

FIXME: missing

#### Proof of Associativity

By the principle of mathematical induction:

Hypothesis: (a+b)+c = a+(b+c)

Base: (a+b)+0 = a+(b+0)

Proof: (a+b)+0 = [by AP1] a+b = [by AP1] a+(b+0).

Induction step: (a+b)+c^{+} = a+(b+c^{+})

Proof:

- (a+b)+c
^{+} = [by AP2] ((a+b)+c)^{+} = [by hypothesis]
- (a+(b+c))
^{+} = [by AP2] a+(b+c)^{+} = [by AP2]
- a+(b+c
^{+})

#### Proof of Commutativity

The principle of mathematical induction has to be employed twice:

- Hypothesis: a
^{+}+b = (a+b)^{+}

- Base: a
^{+}+0 = [by AP1] a^{+} = [by AP1] (a+0)^{+}

Proof that: a^{+}+b^{+} = (a+b^{+})^{+}

- a
^{+}+b^{+} = [by AP2] (a^{+}+b)^{+} = [by hypothesis] (a+b)^{+}^{+} = [by AP2] (a+b^{+})^{+}.

Hypothesis: a+b = b+a

Base: a+0=0+a

By [AP1].

Proof that: a+b^{+}=b^{+}+a

- a+b
^{+} = [by AP2] (a+b)^{+} = [by hypothesis]
- (b+a)
^{+} = [by previous proof] b^{+}+a.

FIXME: enhance visibility by nicer formatting