[Lemma 1]

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]
Last updated: $Date: 2003/04/22 17:00:32 $
[Lemma 1]