   Go backward to 4.2 The Integer NumbersGo up to 4 NumbersGo forward to 4.4 The Real Numbers ## 4.3 The Rational Numbers

The integer numbers are not yet closed with respect to all operations. For instance, there does not exist a natural number x with
1 = x*2.
i.e., the quotient 1/2 is undefined.

We therefore introduce a domain Q of rational numbers such that

1. Z can be "embedded" into Q, and
2. 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 cZ the operation c in Z.

First, we need some auxiliary functions.

Definition 44 (Integer Conversions) We define the following conversion functions between natural numbers and integers.
 Z: N -> Z >= 0, Z(x) := ; N: Z -> N, N(x) := |x|0;

It is easy to see that, for every n in N, N(Z(n))=n and, for every i in N, Z(N(i))=|i|.

Definition 45 (Rational Numbers) The set Q of  rational numbers (rationale Zahlen) is the following subset of Z x Z:
Q:= {<x, y>: x in Z /\  y in Z> 0 /\  N(x) and N(y) are relatively prime}.
We define a corresponding constructor function */*: Z x Z> 0 -> Q
x/y := <sign(x *Z y) *Z (|x| divZ g), |y| divZ g>
 where g = Z(gcd(N(x), N(y))).
Let r in Q and take x and y such that r=<x, y>. We call x the  numerator (Zähler) of r and y its  denominator (Nenner):
 numerator(r) := such x: exists y: r in Q /\  r = ; denominator(r) := such y: exists x: r in Q /\  r = .

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

Example  We have for 1 in Z, 2 in Z:
1/2 = <1, 2>, 1/- 2 = <- 1, 2>, 2/2 = <1, 1>.

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

Proposition 46 (Uniqueness) We have for all integers a, b, c, d:
(b != 0Z /\  d != 0Z /\  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 != 0Z /\  c != 0Z) => 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.

Definition 46 (Rational Number Operations)
Constants
0 := 0Z/1Z; 1 := 1Z/1Z; 2 := 2Z/1Z.
Arithmetic
x + y := (x0 *Z y1)+Z (x1*Zy0)/x1*Zy1;
x * y := x0*Zy0/x1*Zy1;
-x := -Z x0/x1;
x - y := x + (-y);
x-1 := x1/x0;
x/y := x * y-1.
Total Order
x <= y : <=> x0 *Z y1 <= Z y0 *Z x1.

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.

Proposition 47 (Quotient) For all rationals x and y != 0 the quotient is defined:
forall x in Q, y in Q\{0}: x = (x/y)*y.

Proof  Take arbitrary x in Q and y in Q\{0}. We have
 (x/y)*y = (definition of /) (x*y-1)*y = (associativity of *) x*(y-1*y) = (*) x*1 = (definition of * and 1) x.
(*) We show y-1*y = 1:
 y-1*y = (definition of -1) y1/y0 * y = (definition of */*) * y = (def. *, g != 0) (sign(y1 *Z y0) *Z (|y1| divZ g)) *Z y0/(|y0| divZ g) *Z y1 = (Prop. Uniqueness, g != 0) sign(y1 *Z y0) *Z |y1| *Z y0/|y0| *Z y1 = (Prop. Uniqueness, y != 0) sign(y1 *Z y0) *Z sign(y0)/sign(y1) = (arithmetic in Z) sign(y1) *Z sign(y0) *Z sign(y0)/sign(y1) = (Pr. Uniqueness, y1 != 0) sign(y0) *Z sign(y0)/1Z = (arithmetic in Z) 1Z/1Z = (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.

Proposition 49 () Between any two rational numbers, there is another rational number:
forall x in Q, y in Q: x < y => exists z in Q: x < z < y.

Proof  Take any x in Q and y in Q with x < y. Then x < (x+y)/2 < 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   