Go backward to 4.3 The Rational Numbers Go up to 4 Numbers Go forward to 4.5 The Complex Numbers |
x * x = 2.i.e., there is no square root of 2 in Q.
forall x in Q: x * x != 2.Take arbitrary x in Q. We assume (1) x * x = 2 and show a contradiction. From the construction of Q, we know x = a/b for some a in Z and b in Z> 0 such that (2) N(a) and N(b) are relatively prime. We have a *Z a/b *Z b = 2 and thus (from now on we operate in Z and drop the corresponding subscripts):
(3) a * a = 2 * b * b.From (3) we know N(2) | N(a*a) and thus also (4) N(2) | N(a) (a proposition that has to be proved extra). Therefore there exists some c in Z such that
(5) a = 2*c.From (3) and (5) we have 2*c*2*c = 2*b*b, i.e., 2*c*c = b*b, thus (6) N(2) | N(b*b) and therefore (7) N(2) | N(b). (4) and (7) contradict (2).
We will now introduce the domain R of real numbers which provides a solution for the equation stated above. While there exist also relatively concrete set-theoretic constructions of R (e.g. as a set of infinite decimal fractions), the usual construction is another instance of the kind that will be stated for Z and Q in Chapter Relations.
In this section, we will characterize R in an inconstructive way by a number of axioms.
x + y = y + x, x + (y + z) = (x + y) + z, x + (-y) = 0, x * y = y * x, x * (y * z) = (x * y) * z, x * (x-1) = 1, x * 1 = x, x * (y + z) = (x * y) + (x * z);
x <= x, x <= y \/ y <= z, (x <= y /\ y <= z) => x <= z, x <= y => x + z <= y + z, (x <= y /\ 0 <= z) => x <= y * z.
Every non-empty subset of R that has an upper bound also has an upper limit.
forall S subset R: S != 0 => ((exists B in R: B is upper bound of S) => (exists L in R: L is upper limit of S)).
The predicates used in the completeness axiom are defined below.
B is upper bound of S : <=> forall x in S: x <= B.An upper limit (obere Grenze) of S is the smallest upper bound of S:
L is upper limit of S : <=> L is upper bound of S /\ (forall M: M is upper bound of S => B <= M).
Intuitively, the completeness axiom makes the real numbers much more "dense" than the rational numbers where above property does not hold.
and ! denotes the factorial function, i.e.,
a: N -> Q a(i) = 1/i!
a = [1/1, 1/1, 1/1*2, 1/1*2*3, 1/1*2*3*4, ...]and
S = {1/1, (1/1+1/1), (1/1+1/1+1/1*2), (1/1+1/1+1/1*2+1/1*2*3), ...}.S has an upper bound 3/1 but no upper limit in Q. However, it has an upper limit in R traditionally denoted by the constant e (= 2.718281828...).
Then we have the following result which implies that the problem stated at the begin of this section can be solved.
forall a in R >= 0, n in N>0: exists x in R: xn = a.
Since we can show that, for every x in R, x * x = x2N, this implies the existence of a square root of 2 in R.
sqrtn(x) := such y: xn = y sqrt(x) := sqrt2N(x).
As a consequence of Proposition Existence of Real Roots, we have
forall a in R >= 0, n in N>0: (sqrtn(a))n = a.
Contiguous subsets of the reals are often denoted as shown below.
For all a in R and b in R, the intervals [a, b] and [a, b[ are called left closed (linksseitig abgeschlossen), and the intervals [a, b] and ]a, b] are called right closed (rechtsseitig abgeschlossen).
[a, b] := {x in R: a <= x <= b}; [a, b[ := {x in R: a <= x < b}; ]a, b] := {x in R: a < x <= b}; ]a, b[ := {x in R: a < x < b}.
Intervals are contiguous in the sense that if two values are in an interval S, then also every intermediate value is in this interval, i.e.,
(forall x in S, y in S: x <= y => (forall z in R: x <= z <= y => z in S)).
The set R "embeds" Q in the sense that will be discussed in Section Embedding Sets. However, unlike the relationship between Z and Q (which are essentially of the "same" size), there are considerably "more" reals than there are rationals. Actually we will see in Section Counting Set Elements that there are so many elements of R that this set cannot be represented in a computer even with an infinite number of memory cells.
Consequently the Logic Evaluator does in file real.txt
not implement the reals but fakes real number operations (without square root
computation) by rational number operations .
In Chapter Relations we will sketch a "structurally equal" construction that is an instance of the general technique that can be applied for the construction of Z, and Q.