Addition in N

This article assumes N to exclude 0

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 Peano postulates.

The Axioms

• a⁺ = a+1
  
• 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 principal of Mathematical induction:

Hypothesis: (a+b)+c = a+(b+c)
Base: (a+b)+1 = a+(b+1)
This is part of the axioms. So this statement holds.

Proof that: (a+b)+c⁺ = a+(b+c⁺)

(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 principal of Mathematical induction has to be employed twice:

Hypothesis: a+1 = 1+a
Base: 1+1 = 1+1
This statement holds.

Proof that: a⁺+1 = 1+a⁺

a⁺+1 = [by AP1] (a+1)+1 = [by associativity] a+(1+1) = [by hypothesis] = (1+1)+a = [by associativity] = 1+(1+a) = [by hypothesis] 1+(a+1) = [by AP1] = 1+a⁺

As a⁺+1 = 1+a⁺ is proofen, it is used as the next base for the induction.

Hypothesis: a+b = b+a
Base: a+1=1+a
Proof that: a+b⁺=b⁺+a

a+b⁺ = [by AP2] (a+b)⁺ = [by hypothesis] (b+a)⁺ = [by AP2] (b+a⁺) = [by AP1] (b+(a+1)) = [by base case] (b+(1+a) = [by associativity] (b+1)+a = [by AP1] b⁺+a

FIXME: enhance visibility by nicer formatting