Go backward to 7.1.2 Modular Arithmetic Go up to 7.1 Equivalence Relations and Partitions

7.1.3 Another Construction of Number Domains

x ~ Z y : <=> (x0 +N y1 = y0 +N x1)

Z:= (N x N)/ ~ Z

0 := [<0N, 0N>]; 1 := [<1N, 0N>]; 2 := [<2N, 0N>]

x := such a in N x N: x = [a]

x + y	:=	[<x0+Ny0,x1+Ny1>]
- x	:=	[<x1,x0>]
x - y	:=	[<x0+Ny1,y0+Nx1>]
x * y	:=	[<(x0*Ny0)+N(x1*Ny1), (x0*Ny1)+N(x1*Ny0)>]
x <= y	: <=>	x0+y1 <= N y0+x1

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.

i: Z' -> Z

i(x) := [x]

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

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

j: Z -> Z'

j(x) := I(x)

i(x+Z'y) = x+Zy.

i(x+Z'y)

=

i(I(x0 +N y0, x1 +N y1)).

Case x₀ +_N y₀ >= x₁ +_N y₁:

We have

i(I(x0 +N y0, x1 +N y1))	=
i(<(x0 +N y0) - (x1 +N y1)>)	=
[<(x0 +N y0) - (x1 +N y1)>]	=	(definition  ~ Z)
[<x0 +N y0, x1 +N y1>]	=
x +Z y.

Case x₀ +_N y₀ < x₁ +_N y₁:

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 : <=> (x0 *Z y1 = y0 *Z x1)

Q:= (Z x Z != 0)/ ~ Q

0 := [<0Z, 1Z>]; 1 := [<1Z, 1Z>]; 2 := [<2Z, 1Z>];

x := such a in Z x Z: x = [a]

x + y	:=	[<(x0 *Z y1) +Z (y0 *Z x1), x1 *Z y1>]
- x	:=	[<-Z x0, x1>]
x - y	:=	[<(x0 *Z y1) -Z (y0 *Z x1), x1 *Z y1>]
x * y	:=	[<x0 *Z y0, x1 *Z y1>]
x-1	:=	[<x1, x0>]
x/y	:=	[<x0 *Z y1, y0 *Z x1>]
x <= y	: <=>	x0 *Z y1 <= Z y0 *Z x1

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.

i: Q' -> Q

i(x) := [x]

i(0Q')	=	0Q,
i(x+Q'y)	=	x+Qy,
i(-Q' x)	=	-Q x,
i(x-Q'y)	=	x-Qy,
i(x*Q'y)	=	x*Qy,
i(x-1)	=	x-1,
i(x/Q'y)	=	x/Qy,
x <= Q' y	<=>	i(x) <= Q i(y).

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

j: Q -> Q'

j(x) := x0/x1

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.

f is Cauchy-sequence: <=>

f: N -> Q /\

forall epsilon in Q>0: exists N in N: forall m >= N, n >= N: |fm-fn| < 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 :

f ~ R g : <=> forall epsilon in Q>0: exists N in N: forall n >= N: |fn - gn| < epsilon .

C := {f: N -> Q: f is Cauchy-sequence}

R:= C/ ~ R

0	:=	[such f in C: forall n in N: fn = 0Q]
1	:=	[such f in C: forall n in N: fn = 1Q]
2	:=	[such f in C: forall n in N: fn = 2Q]

x := such f in C: x = [f]

x + y	:=	[[xn +Q yn]n]
- x	:=	[[-Q xn]n]
x - y	:=	[[xn -Q yn]n]
x * y	:=	[[xn *Q yn]n]
x-1	:=	[[xn-1]n]
x / y	:=	[[xn /Q yn]n]
x is positive	: <=>	exists epsilon in Q> 0, N in N: forall n >= N: x > epsilon
x <= y	: <=>	exists z in R: z is 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²+1 (the polynomial that defines the imaginary unit). We omit the details.