[FOM] Re: FOM and real numbers

[Roger Bishop Jones]

Rob Arthan, who is not a fom subscriber, has asked me to forward
the following message to FOM.
================================================================

Roger Jones has kindly drawn my attention to this interesting 
post by Andreas 
Blass. It may be of interest that developing the theory of reals 
conservatively using a mechanized tool such as HOL has led 
several people to  
consider constructions that are logically more streamlined than 
the 
conventional routes via the rational numbers. Apart from its 
intrinsic 
interest, much of the point of this is to avoid the large 
numbers of case 
splits that appear when the usual constructions are carried out 
with complete 
rigour. As Conway says in "On Numbers and Games", some 
presentations involve 
lemmas with as many as 64 cases.

In his pioneering work on the foundations of analysis in HOL, 
John Harrison 
essentially rediscovered Schanuel's construction much as 
described by 
Andreas. John's construction actually starts from the natural 
numbers rather 
than the integers and proceeds to construct the positive reals 
as an 
algebraic system in its own right. The field R is then 
constructed in the 
obvious way and systems like the rationals and the integers can 
be found 
inside the result. This is all written up in John's thesis, 
which has since 
been published as a book.

[see: http://www.cl.cam.ac.uk/users/jrh/papers.html (RBJ)]

When I embarked on a construction of the reals for 
ProofPower-HOL, my starting 
point was somewhat different - I had a well-developed and 
tool-supported 
theory of the integers, not just the natural numbers. My 
thinking was that 
the order structure of the real numbers appear as the 
Dedekind-MacNeille 
completion of any dense subgroup of the additive group of reals. 
The additive 
group of reals has lots of dense subgroups, and many of them are 
algebraically much simpler than the rationals and can easily be 
constructed 
from first principles using the integers.

The additive structure is easy to define a la Dedekind, provided 
you can show 
that the ordering makes the subgroup dense and archimedean. The 
multiplicative structure can then be derived by a construction 
essentially 
going back to Hoelder in 1901, amounting to an analysis of the 
order-preserving endomorphisms of the additive group showing 
that for any 
positive x, there is a unique such endomorphism that sends a 
chosen positive 
unit element, 1, to x - and that endomorphism is multiplication 
by x.

This then just leaves you having to find a convenient dense 
subgroup of R that 
can be constructed conveniently from the integers. My first go 
at this was to 
try Z[sqrt(2)], i.e., numbers of the form a + b sqrt(2) with a 
and b 
integers. The addition of these is trivial to define, but I had 
some problems 
with giving a tractable definition of the ordering relation (the 
main problem 
is set as an exercise in MacLane and Birkhoff's book on algebra, 
but a naive 
algebraic proof involves lots of tedious case splits, resulting 
in a 
collection of quadratic diophantine inequalities, most of which 
require some 
ingenuity to prove).

My first successful go in ProofPower-HOL used the multiplicative 
monoid of 
dyadic rationals instead (and a harder argument, because that 
monoid is not a 
group).

I later found a novel way to define the ordering on Z[sqrt(2)] 
which leads to 
delightfully short proofs that Z[sqrt(2)] is dense and 
archimedean. Like 
Schanuel's construction, only the additive and order structure 
of the 
integers is needed to develop the additive and order structure 
of the reals. 
Indeed, you can probably usefully develop some elementary 
calculus before 
developing the multiplicative theory (e.g., the intermediate 
value theorem 
could very usefully be proved at this stage).

My construction using Z[sqrt(2)] is written up in a paper "An 
Irrational 
construction of R from Z" that can be found by following a link 
on 
http://www.lemma-one.com/papers/papers.html.

I note that Andreas suggests that you need the multiplicative 
structure to 
prove that these constructions lead to something isomorphic to 
the usual 
constructions. However, I think that can probably be bypassed. 
If memory 
serves, the relevant arguments are all given in the 1956 paper 
of Behrend 
referenced in my paper.

Regards,

Rob Arthan (rda at lemma-one.com)