Go backward to 7.1.2 Modular ArithmeticGo up to 7.1 Equivalence Relations and Partitions |

x~_{Z}y: <=> (x_{0}+_{N}y_{1}=y_{0}+_{N}x_{1})Z:= (NxN)/ ~_{Z}0 := [<0 _{N}, 0_{N}>]; 1 := [<1_{N}, 0_{N}>]; 2 := [<2_{N}, 0_{N}>]:=xsuchainNxN:x= [a]

x+y:= [< x_{0}+_{N}y_{0},x_{1}+_{N}y_{1}>]- x:= [< x_{1},x_{0}>]x-y:= [< x_{0}+_{N}y_{1},y_{0}+_{N}x_{1}>]x*y:= [<( x_{0}*_{N}y_{0})+_{N}(x_{1}*_{N}y_{1}), (x_{0}*_{N}y_{1})+_{N}(x_{1}*_{N}y_{0})>]x<=y: <=> x_{0}+y_{1}<=_{N}y_{0}+x_{1}

In above definition, [`x`] denotes [`x`]_{ ~ Z}.
It is easy to see that ~ _{Z} is an equivalence relation, therefore
**Z** is a partition of **N** x **N**. The corresponding equivalence
classes satisfy congruence properties similar to those of
Proposition *Congruence Properties* such that the
results of all operations are uniquely defined.

5 = [<7,2>] = {<5, 0>, <6, 1>, <7, 2>, <8, 3>, ...} -6 = [<3,9>] = {<0, 6>, <1, 7>, <2, 8>, <3, 9>, ...} 5+(-6) = [<7,2>] + [<3,9>] = [<10, 11>] = [<0, 1>] = -1 5*(-6) = [<7,2>] * [<3,9>] = [<39, 69>] = [<0, 30>] = -30 5 <= -6 <=> [<7,2>] <= [<3,9>] <=> 16 <= 5 <=> F.

The new construction is isomorphic to the old one such that the properties of all operations are preserved.

is an isomorphism with respect to 0, +, -, *, <, i.e.,

i:Z' ->Zi(x) := [x]

i(0_{Z'})= 0 _{Z},i(x+_{Z'}y)= x+_{Z}y,i(-_{Z'}x)= - _{Z}x,i(x-_{Z'}y)= x-_{Z}y,i(x*_{Z'}y)= x*_{Z}y,x<=_{Z'}y<=> i(x) <=_{Z}i(y).

It is easy to see that the inverse isomorphism is denoted by

where "I" denotes the constructor function on

j:Z->Z'j(x) := I()x

We know

i(x+_{Z'}y) =x+_{Z}y.

i(x+_{Z'}y)= i(I(x_{0}+_{N}y_{0},x_{1}+_{N}y_{1})).

**Case**`x`_{0}+_{N}`y`_{0}>=`x`_{1}+_{N}`y`_{1}:-
We have
`i`(I(`x`_{0}+_{N}`y`_{0},`x`_{1}+_{N}`y`_{1}))= `i`(<(`x`_{0}+_{N}`y`_{0}) - (`x`_{1}+_{N}`y`_{1})>)= [<( `x`_{0}+_{N}`y`_{0}) - (`x`_{1}+_{N}`y`_{1})>]= (definition ~ _{Z})[< `x`_{0}+_{N}`y`_{0},`x`_{1}+_{N}`y`_{1}>]= `x`+_{Z}`y`. **Case**`x`_{0}+_{N}`y`_{0}<`x`_{1}+_{N}`y`_{1}:- Proceeds analogously.

An implementation of this construction in the Logic Evaluator is shown below,
see Appendix * integer2.txt*.

**Rational Numbers**
In Section *The Rational Numbers*, we have defined a rational
as a pair <`x`, `y`> of integer numbers `x` and
`y` such that their quotient denotes the desired value. In order
to determine this pair uniquely, `x` and `y` have been chosen
relatively prime with `y` being positive. We will now lift this
restriction by defining a rational as the class of all pairs with the same
quotient.

x~_{Q}y: <=> (x_{0}*_{Z}y_{1}=y_{0}*_{Z}x_{1})Q:= (ZxZ_{ != 0})/ ~_{Q}0 := [<0 _{Z}, 1_{Z}>]; 1 := [<1_{Z}, 1_{Z}>]; 2 := [<2_{Z}, 1_{Z}>];:=xsuchainZxZ:x= [a]

x+y:= [<( x_{0}*_{Z}y_{1}) +_{Z}(y_{0}*_{Z}x_{1}),x_{1}*_{Z}y_{1}>]- x:= [<- _{Z}x_{0},x_{1}>]x-y:= [<( x_{0}*_{Z}y_{1}) -_{Z}(y_{0}*_{Z}x_{1}),x_{1}*_{Z}y_{1}>]x*y:= [< x_{0}*_{Z}y_{0},x_{1}*_{Z}y_{1}>]x^{-1}:= [< x_{1},x_{0}>]x/y:= [< x_{0}*_{Z}y_{1},y_{0}*_{Z}x_{1}>]x<=y: <=> x_{0}*_{Z}y_{1}<=_{Z}y_{0}*_{Z}x_{1}

It is easy to see that ~ _{Q} is an equivalence relation on **Z** x **Z**_{ != 0} where **Z**_{ != 0} := {`x` in **Z**: `x` != 0}; we have a corresponding partition that also
satisfies the necessary congruence properties such that the results of all
operations are uniquely defined.

4/6 = [<4, 6>] = {<2, 3>, <-2, -3>, <4, 6>, <-4, -6>, <6, 9>, ...} -2/5 = -[<2, 5>] = [<-2, 5>] = {<2, -5>, <-2, 5>, <4, -10>, <-4, 10>, <6, -15>, ...} 4/6 + (-2/5) = [<4, 6>] + [<-2, 5>] = [<8, 30>] = [<4, 15>] = 4/15 4/6 * (-2/5) = [<4, 6>] * [<-2, 5>] = [<-8, 30>] = [<-4, 15>] = -4/15

Again the new construction is isomorphic to the old one such that the properties of all operations are preserved.

is an isomorphism with respect to 0, +, -, *, ', <, i.e.,

i:Q' ->Qi(x) := [x]

i(0_{Q'})= 0 _{Q},i(x+_{Q'}y)= x+_{Q}y,i(-_{Q'}x)= - _{Q}x,i(x-_{Q'}y)= x-_{Q}y,i(x*_{Q'}y)= x*_{Q}y,i(x^{-1})= x^{-1},i(x/_{Q'}y)= x/_{Q}y,x<=_{Q'}y<=> i(x) <=_{Q}i(y).

It is easy to see that the inverse isomorphism is denoted by

where */* denotes the constructor function on

j:Q->Q'j(x) :=x_{0}/x_{1}

An implementation of this construction in the Logic Evaluator is shown
below,
see Appendix * rational2.txt*.

**Real Numbers**
While in Section *The Real Numbers* the real numbers have
been only axiomatically characterized, also a direct construction is
possible. The square of no rational number yields 2, but can define an
infinite *sequence* of rationals that approaches such a number
arbitrarily closely. The basic idea is to partition the set of all
"well-behaved" infinite sequences of rationals by an equivalence relation
that is true for any two sequences that approach each other arbitrarily
closely. Each such equivalence class denotes a real number with arithmetic
being defined point-wise on the sequence.

For this construction, we first define the class of "well-behaved" sequences.

fis Cauchy-sequence: <=>f:N->Q/\forallepsilon inQ_{>0}:existsNinN:forallm>=N,n>=N: |f_{m}-f_{n}| < epsilon .

In other words, for every epsilon , from a certain position `N` on, all
members of a Cauchy-sequence stay in a "tunnel" of width epsilon :

The position of this tunnel determines a real number; two sequences define the same number if the difference of their corresponding members becomes arbitrarily small. We define this equivalence relation and the arithmetic operations as shown below.

f~_{R}g: <=>forallepsilon inQ_{>0}:existsNinN:foralln>=N: |f_{n}-g_{n}| < epsilon .C:= {f:N->Q:fis Cauchy-sequence}R:=C/ ~_{R}

0 := [ suchfinC:forallninN:f_{n}= 0_{Q}]1 := [ suchfinC:forallninN:f_{n}= 1_{Q}]2 := [ suchfinC:forallninN:f_{n}= 2_{Q}]

:=xsuchfinC:x= [f]

x+y:= [[ x_{n}+_{Q}y_{n}]_{n}]- x:= [[- _{Q}x_{n}]_{n}]x-y:= [[ x_{n}-_{Q}y_{n}]_{n}]x*y:= [[ x_{n}*_{Q}y_{n}]_{n}]x^{-1}:= [[ x_{n}^{-1}]_{n}]x/y:= [[ x_{n}/_{Q}y_{n}]_{n}]xis positive: <=> existsepsilon inQ_{> 0},NinN:foralln>=N:> epsilonxx<=y: <=> existszinR:zis positive /\x+z=y

We use the notation [`T`]_{n} for the sequence `f` defined
as `f`(`n`) := `T` (not to confuse with the notation
[`x`] for the equivalence class of `x`). One can show that
~ _{R} is an equivalence relation that satisfies the necessary
congruence properties to determine unique result values for the functions
defined above. Furthermore, one can show that the domain **R** defined in
such a way satisfies the axioms stated in Section *The Real
Numbers*, i.e., we have indeed the real numbers.

**Complex Numbers** Also **C** can be defined along the lines
demonstrated above. The intuition is to partition the set of all univariate
polynomials (considered as equations with righthand side zero) by the
equivalence relation that is true for two polynomials if their difference is
divisible by `x`^{2}+1 (the polynomial that defines the imaginary unit).
We omit the details.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999