   Go backward to 4.1 The Natural NumbersGo up to 4 NumbersGo forward to 4.3 The Rational Numbers ## 4.2 The Integer Numbers

As we have seen in the previous section, the domain of natural numbers is "open" in the sense that, for certain arguments, some important operations have no value in this domain. For instance, there does not exist a natural number x with
0 = x+1,
i.e., (0-1) is undefined.

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 cN the function or predicate c in N.

Definition 42 (Integer Numbers) The set Z of  integer numbers (ganze Zahlen) is defined as the following subset of N×N:
 Z:= Z >= 0 union Z< 0; Z >= 0 := {: x in N}; Z< 0 := {<0N, x>: x in N\{0N}}; Z> 0 := Z >= 0\{<0N, 0N>}.
We define a corresponding constructor function:
 I: N x N -> Z I(x, y) := if x >= N y then else <0N, y-Nx>;

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

Definition 43 (Integer Operations)
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 := ; x - y := x + (-y).
Total Order
 x <= y : <=> (x0+y1
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.

Proof  We show
forall x in Z, y in Z: x+y = y+x.
Take arbitrary x in Z,y in Z. We have
 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.

Proposition 44 (Difference) For every integer x and y the difference is defined:
forall x in Z, y in Z: x = (x-y)+y.

Proof  Take arbitrary x in Z and y in Z. We have
 (x-y)+y = (definition of -) (x+(-y))+y = (associativity of+) x+((-y+y)) = (*) x+0 = (definition of + and 0) x.
(*) We show -y+y = 0:
 -y+y = (definition of -) +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.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   