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

0 =i.e., (0-1) is undefined.x+1,

We therefore introduce a domain **Z** of *integer numbers* such that

**N**can be "embedded" into**Z**, and- 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**.

We define a corresponding constructor function:

Z:=Z_{ >= 0}unionZ_{< 0};Z_{ >= 0}:= {<x, 0_{N}>:xinN};Z_{< 0}:= {<0_{N},x>:xinN\{0_{N}}};Z_{> 0}:=Z_{ >= 0}\{<0_{N}, 0_{N}>}.

I: NxN->ZI( x,y) :=ifx>=_{N}ythen<x-_{N}y, 0_{N}>else<0_{N},y-_{N}x>;

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(0 _{N}, 0_{N}); 1 := I(1_{N}, 0_{N}); 2 := I(2_{N}, 0_{N}).**Basic Arithmetic**`x`+`y`:= I(`x`_{0}+_{N}`y`_{0},`x`_{1}+_{N}`y`_{1});`x`*`y`:= I((`x`_{0}*_{N}`y`_{0}) +_{N}(`x`_{1}*_{N}`y`_{1}), (`x`_{0}*_{N}`y`_{1}) +_{N}(`x`_{1}*_{N}`y`_{0}));- `x`:= <`x`_{1},`x`_{0}>;`x`-`y`:=`x`+ (-`y`).**Total Order**`x`<=`y`: <=> (`x`_{0}+`y`_{1}<_{N}`y`_{0}+`x`_{1}).**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.

Take arbitraryforallxinZ,yinZ:x+y=y+x.

x+y= (definition of +) I( x_{0}+_{N}y_{0},x_{1}+_{N}y_{1})= (commutativity of + _{N})I( y_{0}+_{N}x_{0},y_{1}+_{N}x_{1})= (definition of +) y+x.

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

forallxinZ,yinZ:x= (x-y)+y.

(*) We show -

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

- y+y= (definition of -) < y_{1},y_{0}>+y= (definition of +) I( y_{1}+_{N}y_{0},y_{0}+_{N}y_{1})= (definition of I, computation in N)(0 _{N}, 0_{N})= (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