previous up next
Go up to 4 Numbers
Go forward to 4.2 The Integer Numbers
RISC-Linz logo

4.1 The Natural Numbers

Intuitively, the natural numbers are the numbers of counting distinct objects: there may be no object, one object, two objects, .... While the domain of natural numbers looks very simple and familiar, it is surprisingly powerful; e.g. every computer program can be encoded as a natural number. However, only  discrete realities can be described by natural numbers; there are also  continuous realities where the distinction between objects is so "fine" that they cannot be modelled by this domain.

Peano Arithmetic  We may consider the natural numbers as an elementary domain by a theory that is due to the mathematician Peano.

Axiom 3 (Peano Arithmetic) The theory of natural numbers has an object constant 0 ( zero) and a unary function constant ', the  successor (Nachfolger), that satisfy the following axioms.
  1. 0 is not the successor of any natural number:
    forall x: x' != 0.
  2. Different natural numbers have different successors:
    forall x, y: x' = y' => x = y.
  3. For every formula F, we have an axiom that states: F holds for every natural number, if F holds for 0 and with every number also for its successor, i.e.,
    (F[x <- 0] /\  (forall x: F => F[x <- x+1])) => forall x: F.
    We call these axioms the  induction axioms (Induktionsaxiome).

The Peano axioms essentially state that the natural numbers are a single infinite chain

0 -> 0' -> 0" -> 0"' -> ...
We will see later how all operations on the natural numbers can be defined just on the basis of 0 and '.

Construction from Sets  It is not necessary to consider the natural numbers as elementary objects; they can be defined within the framework of set theory that provides a more fundamental kind of objects.

Definition 33 (Natural Numbers from Set) We define a constant 0 and a unary function ' as follows:
0 := 0;
x' := x union {x}.

The first two axioms of Peano arithmetic are consequences of this definition.

Proof  We sketch the proof of the first two laws of Peano.

The construction of natural numbers proceeds with the definition of a set N (which we do not give) such that the following proposition holds.

Proposition 38 (Natural Numbers)  N, the set of  natural numbers (natürliche Zahlen), is the smallest set that satisfies the following properties:
0 in N;
forall x in N: x' in N;
for every formula F:
   (F(0) /\  forall x in N: F(x) => F(x+1)) => forall x in N: F(x).

Thus also the third law of Peano holds in the set-based construction of natural numbers. Sometimes the following notations will be used.

Definition 34 (Natural Number Subsets) 
N>0 := {x in N: x > 0};
Nn := {x in N: x < n}.

Arithmetic Operations  Independently of how we have introduced the natural numbers, we can define the basic arithmetic operations with the help of the functions 0 and ' and the following auxiliary operation.

Definition 35 (Predecessor) The  predecessor (Vorgänger) of a natural number x is the natural number whose successor is x:
x- := such y: x = y'.

Because of the second Peano law, the predecessor is uniquely defined (if it exists). However, because of the first Peano law, there is no x such that x' = 0 and thus 0- is undefined (and we must not assume 0-' = 0).

We now introduce the arithmetic operations by recursive definitions. In the rest of this section, all variables denote natural numbers.

Definition 36 (Natural Numbers Operations) We define the following functions and predicates (for all recursive definitions, a corresponding termination function is r(x, y) := y).
1 := 0', 2 := 1';
x + y := if y = 0 then x else (x+y-)'
x * y := if y = 0 then 0 else x+(x*y-)
Total Order
x <= y : <=>
   if x = 0 then T
   else if y = 0 then F
   else x- <= y-

The recursive definitions are constructive in the sense that they can be executed by repeated "unfolding" of the definition.

Example  We compute (1+2):
1+2 = (definitions of 1 and 2)
0' + 0" = = (definition of +)
(if 0" = 0 then 0' else (0'+0"-)') = (second Peano law)
(0'+0"-)' = (definition of -)
(0'+0')' = (definition of +)
(if 0' = 0 then 0' else (0'+0'-)')' = (second Peano law)
(0'+0'-)" = (definition of -)
(0'+0)" = (definition of +)
(if 0 = 0 then 0' else (0'+0-)')" = (reflexivity of =)

Natural Number Laws  Immediate consequences of these definitions are the following laws.

Proposition 39 (Natural Numbers Operations) For all natural numbers x and y, we have:
x + 0 = x,
x + y' = (x+y)';
x * 0 = 0,
x * y' = x+(x*y);
Total Order
0 <= x <=> T,
x <= 0 <=> x = 0,
x' <= y' <=> x <= y.

Furthermore, the following well known laws hold.

Proposition 40 (Natural Number Laws) For all natural numbers x, y, z, we have:
x + 0 = x,
x * 1 = x,
x + y = y + x,
x * y = y * x,
x + (y + z) = (x + y) + z,
x * (y * z) = (x * y) * z,
x * (y + z) = (x * y) + (x * z),
x <= x,
(x <= y /\  y <= x) => x = y,
(x <= y /\  y <= z) => x <= z.

We will use the following abbreviations for every domain that provides a binary predicate <= .

Definition 37 (Order Predicates) 
x < y : <=> x <= y /\  x != y;
x > y : <=> x not  <= y;
x >= y : <=> x not < y.

We often write a <= x < b to denote x <= a /\  x < b and similar for all other combinations of the order predicates.

Logic Evaluator  Although there is a builtin implementation of the natural numbers, we are going to simulate the construction on the base of 0 and and '; we use the letter N to distinguish the natural number function and predicate constants from those that are going to be introduced in the following sections. These and the subsequent definitions are collected in Appendix natural.txt.

More Operations  Since we have addition, we would also like to have the inverse operation.

Definition 38 (Difference)  z is a difference of x and y if x = y+z.
x - y := such z: x = z+y.

Please note that a difference between two natural numbers does not always exist, e.g. 1-2 is undefined because there is no z with 1=z+2 (and we must not assume 1 = (1-2)+2). However, we have the following result.

Proposition 41 (Difference) If a difference exists, it is unique:
forall x, y, z0, z1: (x = z0+y /\  x = z1+y) => z0 = z1.
If x >= y, the difference of x and y is defined:
forall x, y: x >= y => x= (x-y)+y.

At the moment, we state these propositions without proofs. In Chapter Induction, we will discuss in detail how to prove properties about natural numbers.

While the natural numbers do not have an operation for exact division, they provide the following pair of functions.

Definition 39 (Quotient and Remainder) The  quotient (Quotient) and  remainder (Rest) of two natural numbers are defined as follows:
x div y := such q: exists r: r < y /\  x=(q*y)+r;
x mod y := such r: exists q: r < y /\  x=(q*y)+r.

By above definition (x div 0) and (x mod 0) are undefined for every x. On the other side, we have the following positive results.

Proposition 42 (Quotient and Remainder) If quotient respectively remainder of two numbers exist, they are unique.
forall x, y, q0, q1, r0 < y, r1 < y:
   (x=(q0*y)+r0 /\  x=(q1*y)+r1) => (q0 = q1 /\  r0 = r1).
If the divisor is not null, quotient and remainder exist:
forall x, y != 0: (exists q, r: r < y /\  x = (q*y)+r).
We thus have the following relationship between quotient and remainder:
forall x, y != 0: x = (x div y)*y + (x mod y).

We define exponentiation as shown below.

Definition 40 (Exponentiation) We define recursively with termination function r(x, n) := n:
..: N x N -> N,
xn := if n = 0 then 1 else x * xn-.

A corresponding construction can be applied in every domain D with a constant 1 and a binary function * such as the number domains that will be introduced in the following sections; we will then assume the existence of a corresponding function ..: D x N -> D.

Logic Evaluator  Difference, quotient, remainder and exponentiation are defined as shown below.

Other important notions on natural numbers can be introduced as follows.

Definition 41 (Natural Number Operations) 

The definition of prime numbers is motivated by the fact that every positive natural number n has a unique prime number factorization (which will be stated formally in Proposition Prime Number Factorization).

Logic Evaluator  Above notions are defined as shown below (to speed up computation, we we revert to builtin natural number arithmetic using the file natural0.txt.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next