Addition of natural numbers

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