Dear members,

Here is another, considerably simpler approach to working with real
numbers in DC Proof. Rather than constructing the reals starting
with Peano's Axioms for the natural numbers (a HUGE undertaking!),
here we do the opposite -- we start with the axioms for real numbers
R, as presented in most introductory texts, and construct the
natural numbers FROM them. We take a subset of R and prove that it
uniquely exhibits properties equivalent to PA. The natural numbers,
it turns out, are already imbedded in any complete ordered field
(like the real numbers). In my experience, this is not readily
apparent in most texts.

I will be including this proof, along with the proofs of the various
lemmas therein, and other samples of proofs about the real numbers
in a future release of DC Proof.

DC Proof format -- click to download:

http://www.dcproof.com/ConstructN.proof


HTML formal:

http://www.dcproof.com/ConstructN.html

Dan