
Constructing The Real Numbers

This page will eventually contain demo
versions of a construction of the
real numbers in ProofPower along the
lines of the paper An Irrational Construction of R from Z
to be presented at
TPHOLs 2001.
At present there is just a
document giving
the definitions, statements and proofs
relating to the new results in the paper (viz.
a proof based on integer arithmetic alone
that Z[Ö2] is an archimedean, dense ordered ring).
Created by Rob Arthan

Last updated: $Date: 2003/04/22 17:00:32 $


