Go backward to 4.3 The Rational NumbersGo up to 4 NumbersGo forward to 4.5 The Complex Numbers |

i.e., there is no square root of 2 inx*x= 2.

Take arbitraryforallxinQ:x*x!=2.

(3)From (3) we know N(2) | N(a*a= 2 *b*b.

(5)From (3) and (5) we have 2*a= 2*c.

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.

**Field Axioms (Körperaxiome)**`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`);**Order Axioms (Ordnungsaxiome)**`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`.**Completeness Axiom (Vollständigkeitsaxiom)**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.

AnBis upper bound ofS: <=>forallxinS:x<=B.

Lis upper limit ofS: <=>Lis upper bound ofS/\( forallM:Mis upper bound ofS=>B<=M).

Intuitively, the completeness axiom makes the real numbers much more "dense" than the rational numbers where above property does not hold.

and

a:N->Qa(i) = 1/i!

anda= [1/1, 1/1, 1/1*2, 1/1*2*3, 1/1*2*3*4, ...]

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), ...}.

Then we have the following result which implies that the problem stated at the begin of this section can be solved.

forallainR_{ >= 0},ninN_{>0}:existsxinR:x^{n}=a.

Since we can show that, for every `x` in **R**,
`x` * `x` = `x`^{2N}, this implies the existence of a
square root of 2 in **R**.

sqrt ^{n}(x) :=suchy:x^{n}=ysqrt( x) := sqrt^{2N}(x).

As a consequence of Proposition *Existence of Real Roots*, we
have

forallainR_{ >= 0},ninN_{>0}: (sqrt^{n}(a))^{n}=a.

Contiguous subsets of the reals are often denoted as shown below.

For all

[ a,b] := {xinR:a<=x<=b};[ a,b[ := {xinR:a<=x<b};] a,b] := {xinR:a<x<=b};] a,b[ := {xinR: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.,

(forallxinS,yinS:x<=y=> (forallzinR:x<=z<=y=>zinS)).

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**.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999