Next: Multiplication Up: The natural numbers Previous: The natural numbers   Contents

Definition 6.1.7   We call addition the operation in denoted by and defined by the two following conditions:
(A1)
.
(A2)
.
The number is called the sum of and .

Proposition 6.1.8   For any natural number , .

Proof. For any natural number , .

So we have: . It was worth to learn all the stuff until this point!

Proposition 6.1.9   The addition is well-defined.

Proof. The proposition means that the sum is defined for every pair of natural numbers, and that there exists a unique operation verifying the con ditions of definition 1.7. Fix the number and consider the set of the natural numbers for which the sum is computable.
• By definition, .
• Suppose that is a natural number for which the sum is computable. Then we have , i.e. the sum is computable, i.e. .
By the Induction Principle, .

Proposition 6.1.10 (Associative Law)   For any triple of natural numbers, .

Proof. By induction on .
• For , we have:

• Suppose that the property is true for some natural number . Then we have:

Lemma 6.1.11   For any natural number , we have .

We prove the lemma by induction on :
• For , the equality is obvious.
• Suppose that for some natural number . Then we have:

Lemma 6.1.12   For any natural number , we have .

We prove the lemma by induction on :
• For , the equality is obvious.
• Suppose that for some natural number . The we have:

Now we can prove the commutative law:

Proposition 6.1.13 (Commutative Law)   For every pair of natural numbers, we have: .

Proof. By induction on :
• For any natural number , we have , by Lemma 1.11.
• Suppose that the equation holds for some natural number . Then we have:

A direct consequence of the definition of the addition and of the commutative law is as follows:

Corollary 6.1.14 (Neutral element)   For any natural number , .

Proposition 6.1.15 (Cancellation)   For any triple of natural numbers,

Proof. The is trivial. We prove by induction on :
• For , the property is obvious.
• Suppose that for some natural number and for any pair of natural numbers the given implication holds. Then we have:

Proposition 1.15 is particularly important: we cannot use substraction for cancelling in both sides of the equation , because we have not defined such an operation. In fact, it is impossible to define substraction in ; the definition of the substraction has to wait for the construction of the set of the integers and of the operations in (v.i. 2).

Proposition 6.1.16   For any pair of natural numbers,

Proof. The is trivial. We prove by induction on :
• For , the property is obvious.
• Let ; then there exists a natural number such that . The we have:

If , then the predecessor of 0, and this does not exist. Therefore . We proved that if , then for any natural number , . This is the contrapositive expression of the desired result.

Next: Multiplication Up: The natural numbers Previous: The natural numbers   Contents
root 2002-06-10