![[Lemma 1]](../lemma1.gif)
|
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 ![[rda at lemma-one dot com]](../email.gif)
|
Last updated: $Date: 2003/04/22 17:00:32 $
|
|
|