Dear members,

I have been working on possible enhancements to DC Proof that I hope will make
it easier to create recursive definitions of sets and
functions. This has been a major hurdle in the construction of the
real numbers from N.

Download a simple example that makes use of a kind quasi-recursive
definition for the set of odd numbers:

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

This proof makes use of the so-called method of impredicative
comprehension. I show that the number 2 is not an odd number -- not
an earth-shattering result, but it illustrates an important method
of proof. I am considering creating a shortcut to incorporate this
method into the DC Proof program. I am currently working on various
theoretical aspects -- some kind of general theorem of recursion
will have to be established using the current DC Proof system. Your
thoughts on this would be appreciated.

Regards,
Dan Christensen