Go backward to 4.2 The Integer Numbers Go up to 4 Numbers Go forward to 4.4 The Real Numbers |
1 = x*2.i.e., the quotient 1/2 is undefined.
We therefore introduce a domain Q of rational numbers such that
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.
Z: N -> Z >= 0, Z(x) := <x, 0N>; N: Z -> N, N(x) := |x|0;
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>
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):
where g = Z(gcd(N(x), N(y))).
numerator(r) := such x: exists y: r in Q /\ r = <x, y>; denominator(r) := such y: exists x: r in Q /\ 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 != 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.
0 := 0Z/1Z; 1 := 1Z/1Z; 2 := 2Z/1Z.
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.
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.
forall x in Q, y in Q\{0}: x = (x/y)*y.
(*) We show y-1*y = 1:
(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) y1/y0 * y = (definition of */*) <sign(y1 *Z y0) *Z (|y1| divZ g), |y0| divZ g> * 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.
forall x in Q, y in Q: x < y => exists z in Q: 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.