Go backward to 4.1 The Natural Numbers Go up to 4 Numbers Go forward to 4.3 The Rational Numbers

4.2 The Integer Numbers

0 = x+1,

We therefore introduce a domain Z of integer numbers such that

1. N can be "embedded" into Z, and
2. for all integers a and b there is an integer x with a = x+b (and consequently a-b is defined).

We are going to give a corresponding set-theoretic construction of Z that meets these requirements. For the purpose of this endeavor (which is based on the construction of the naturals given in the previous section), we will denote by a constant c_N the function or predicate c in N.

Z:= Z >= 0 union Z< 0;

Z >= 0 := {<x, 0N>: x in N};

Z< 0 := {<0N, x>: x in N\{0N}};

Z> 0 := Z >= 0\{<0N, 0N>}.

I: N x N -> Z

I(x, y) := if x >= N y then <x-Ny, 0N> else <0N, y-Nx>;

The intuition of this construction is that a tuple <a, 0_N> represents a non-negative integer a, while a tuple <0_N, b> represents a negative integer -b. This particular representation has the advantage that the definition of the arithmetic operations on integers becomes relatively easy.

Constants

0 := I(0N, 0N); 1 := I(1N, 0N); 2 := I(2N, 0N).

Basic Arithmetic

x + y := I(x0 +N y0, x1 +N y1);

x * y := I((x0 *N y0) +N (x1 *N y1), (x0 *N y1) +N (x1 *N y0));

-x := <x1, x0>;

x - y := x + (-y).

Total Order

x <= y : <=> (x0+y1 <N y0+x1).

More Arithmetic

|x| := if 0 <= x then x else -x;

sign(x) := if x = 0 then 0 else if 0 <= x then 1 else -1;

x div y := such q: exists r:

|r| < |y| /\  x=q*y+r /\  (sign(r) = 0 \/ sign(r)=sign(y));

x mod y := such r: exists q:

|r| < |y| /\  x=q*y+r /\  (sign(r) = 0 \/ sign(r)=sign(y)).

Logic Evaluator  The implementation of basic arithmetic correspond to the mathematical definitions (see Appendix integer.txt).

For the implementation of quotient and remainder, we need to define the "search range" using an auxiliary function.

One can now show that the operations satisfy the laws stated for their counterparts in N (Propositions Natural Number Operations 1, Difference, and Quotient and Remainder); we give an example.

forall x in Z, y in Z: x+y = y+x.

x+y	=	(definition of +)
I(x0 +N y0, x1 +N y1)	=	(commutativity of +N)
I(y0 +N x0, y1 +N x1)	=	(definition of +)
y+x.

In addition, however, the domain Z is closed with respect to the computation of differences.

forall x in Z, y in Z: x = (x-y)+y.

(x-y)+y	=	(definition of -)
(x+(-y))+y	=	(associativity of+)
x+((-y+y))	=	(*)
x+0	=	(definition of + and 0)
x.

-y+y	=	(definition of -)
<y1, y0>+y	=	(definition of +)
I(y1 +N y0, y0 +N y1)	=	(definition of I, computation in N)
(0N, 0N)	=	(definition of 0)
0.

Thus our definition of Z meets one of the two requirements stated at the begin of this section. In what sense also the other requirement (the embedding of N into Z) is met will be discussed in Section Embedding Sets. Despite the fact that such an embedding is possible, we will also see in Section Counting Set Elements that there are actually no "more" integer numbers than natural numbers.

We will give in Chapter Relations another construction of Z which is in some sense "structurally equal" to the definition above but mathematically more elegant (because it is an instance of a more general technique that can be applied in many situations). The definition above however has the advantage that it is  constructive, i.e., it gives rise to algorithms that can be used for implementation on a computer.