Go up to 4 Numbers Go forward to 4.2 The Integer Numbers |
Peano Arithmetic We may consider the natural numbers as an elementary domain by a theory that is due to the mathematician Peano.
forall x: x' != 0.
forall x, y: x' = y' => x = y.
(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.
0 := 0; x' := x union {x}.
The first two axioms of Peano arithmetic are consequences of this definition.
x union {x} != 0which is true because x in (x union {x}) but x != 0.
(1) x' = y'and have to show x = y. We assume (2) x != y and show a contradiction. From (1), we know by the definition of '
(3) x union {x} = y union {y}.By the definition of union and set enumeration, we know (4) x in x union {x} and (5) y in y union {y}. From (3), (4), and the definition of =, we have (6) x in y union {y} which implies with (2)
(7) x in y.Likewise, we have from (3), (5), and the definition of = that (8) y in x union {x} which implies with (2)
(9) y in x.The conjunction of (7) and (9) is in contradiction to the set-theoretic axiom of regularity (Regularität) that prohibits such "cycles" (in general any infinitely descending chains) with respect to in .
The construction of natural numbers proceeds with the definition of a set N (which we do not give) such that the following proposition holds.
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.
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.
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.
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-)
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.
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 =) 0"'.
Natural Number Laws Immediate consequences of these definitions are the following laws.
x + 0 = x, x + y' = (x+y)';
x * 0 = 0, x * y' = x+(x*y);
0 <= x <=> T, x <= 0 <=> x = 0, x' <= y' <=> x <= y.
Furthermore, the following well known laws hold.
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 <= .
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.
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.
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.
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.
If the divisor is not null, quotient and remainder exist:
forall x, y, q0, q1, r0 < y, r1 < y: (x=(q0*y)+r0 /\ x=(q1*y)+r1) => (q0 = q1 /\ r0 = r1).
We thus have the following relationship between quotient and remainder:
forall x, y != 0: (exists q, r: r < y /\ x = (q*y)+r).
forall x, y != 0: x = (x div y)*y + (x mod y).
We define exponentiation as shown below.
..: 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.
x | y : <=> exists z: x*z = y .
gcd(x, y) := such z: z | x /\ z | y /\ (forall w: (w | x /\ w | y) => w <= z).
lcm(x, y) := such z: x | z /\ y | z /\ (forall w: (x | w /\ y | w) => z <= w).
x and y are relatively prime : <=> gcd(x, y) = 1.
x is prime : <=> x > 1 /\ (forall y: y | x => (y = 1 \/ y = x)).
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
.