Go backward to 4.2 The Integer NumbersGo up to 4 NumbersGo forward to 4.4 The Real Numbers |

1 =i.e., the quotient 1/2 is undefined.x*2.

We therefore introduce a domain **Q** of *rational numbers* such that

**Z**can be "embedded" into**Q**, and- for all integers
`a`and`b`there is an integer`x`with`a`=`x`*`b`(and consequently`a`/`b`is defined).

We proceed by a set-theoretic construction that represents a rational
`r` as a tuple of integers <`x`, `y`> such that
`r`*`y` = `x` (i.e., `r`=`x`/`y`).
In the following, we denote by `c`_{Z} the operation `c` in
**Z**.

First, we need some auxiliary functions.

Z: N->Z_{ >= 0}, Z(x) := <x, 0_{N}>;N: Z->N, N(x) := |x|_{0};

It is easy to see that, for every

We define a corresponding constructor functionQ:= {<x,y>:xinZ/\yinZ_{> 0}/\ N(x) and N(y) are relatively prime}.

x/y:= <sign(x*_{Z}y) *_{Z}(|x| div_{Z}g), |y| div_{Z}g>

Let

whereg= Z(gcd(N(x), N(y))).

numerator( r):= suchx:existsy:rinQ/\r= <x,y>;denominator( r):= suchy:existsx:rinQ/\r= <x,y>.

This construction makes the tuple components relatively prime and places the sign into the first component.

1/2 = <1, 2>, 1/- 2 = <- 1, 2>, 2/2 = <1, 1>.

Consequently, every rational number is represented by a unique tuple.

(b!= 0_{Z}/\d!= 0_{Z}/\a*_{Z}d=b*_{Z}c) =>a/b=c/d.

This gives us the well known simplification rule for every integer
`a`, `b`, and `c`:

(a!= 0_{Z}/\c!= 0_{Z}) =>a*_{Z}b/a*_{Z}c=b/c.

**Logic Evaluator**
The conversion functions and the basic constructors
are implemented as shown below (`@`

`x`, `y` denotes
`x`/`y`); all rational operations are collected in
Appendix * rational.txt*).

We are now ready to define the usual operations on rational numbers.

**Constants**0 := 0

_{Z}/1_{Z}; 1 := 1_{Z}/1_{Z}; 2 := 2_{Z}/1_{Z}.**Arithmetic**`x`+`y`:= (`x`_{0}*_{Z}`y`_{1})+_{Z}(`x`_{1}*_{Z}`y`_{0})/`x`_{1}*_{Z}`y`_{1};`x`*`y`:=`x`_{0}*_{Z}`y`_{0}/`x`_{1}*_{Z}`y`_{1};-

`x`:= -_{Z}`x`_{0}/`x`_{1};`x`-`y`:=`x`+ (-`y`);`x`^{-1}:=`x`_{1}/`x`_{0};`x`/`y`:=`x`*`y`^{-1}.**Total Order**`x`<=`y`: <=>`x`_{0}*_{Z}`y`_{1}<=_{Z}`y`_{0}*_{Z}`x`_{1}.

**Logic Evaluator**
The corresponding executable definitions are listed below.

**Rational Number Laws**
Again we can show that the operations satisfy the
laws stated for their counterparts in **N**
(Propositions *Natural Number Operations*, *Difference*, and
*Quotient and Remainder*).
In addition, however, the domain **Q** is *closed* with
respect to the computation of quotients.

forallxinQ,yinQ\{0}:x= (x/y)*y.

(*) We show

( x/y)*y= (definition of /) ( x*y^{-1})*y= (associativity of *) x*(y^{-1}*y)= (*) x*1= (definition of * and 1) x.

y^{-1}*y= (definition of ^{-1})y_{1}/y_{0}*y= (definition of */*) <sign( y_{1}*_{Z}y_{0}) *_{Z}(|y_{1}| div_{Z}g), |y_{0}| div_{Z}g> *y= (def. *, g!= 0)(sign( y_{1}*_{Z}y_{0}) *_{Z}(|y_{1}| div_{Z}g)) *_{Z}y_{0}/(|y_{0}| div_{Z}g) *_{Z}y_{1}= (Prop. Uniqueness,g!= 0)sign( y_{1}*_{Z}y_{0}) *_{Z}|y_{1}| *_{Z}y_{0}/|y_{0}| *_{Z}y_{1}= (Prop. Uniqueness,y!= 0)sign( y_{1}*_{Z}y_{0}) *_{Z}sign(y_{0})/sign(y_{1})= (arithmetic in Z)sign( y_{1}) *_{Z}sign(y_{0}) *_{Z}sign(y_{0})/sign(y_{1})= (Pr. Uniqueness,y_{1}!= 0)sign( y_{0}) *_{Z}sign(y_{0})/1_{Z}= (arithmetic in Z)1 _{Z}/1_{Z}= (definition of 1) 1.

Our definition of **Q** meets one of the two requirements stated at the begin
of this section. How **Z** is embedded into **Q** will be discussed in
Section *Embedding Sets*. In
Chapter *Relations*, we will give a construction of **Q**
which is "structurally equal" to the definition above (and which is another
instance of the general technique that is used for a corresponding definition
of **Z**).

Another characteristic property that distinguishes **Q** from **Z**
is stated next.

forallxinQ,yinQ:x<y=>existszinQ:x<z<y.

As a consequence, between any two rational numbers there are *infinitely*
many other rational numbers. **Q** can be therefore used for modelling
arbitrarily "fine-grained" realities. However, we will see in
Section *Counting Set Elements* that there are not more
rational numbers than there are integer numbers (or natural numbers).
Furthermore, the next section shows that there are truly "continuous"
realities that cannot be modelled even by rationals.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999