[FOM] Re: FOM and real numbers
Roger Bishop Jones
rbj at rbjones.com
Thu Jul 24 13:02:14 EDT 2003
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)
More information about the FOM
mailing list