Drexel dragonThe Math ForumDonate to the Math Forum

Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.

Math Forum » Discussions » sci.math.* » sci.math

Topic: Formal Proof of Cantor-Bernstein-Schroeder Theorem using DC Proof 2.0
Replies: 2   Last Post: Jun 15, 2013 11:44 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Dan Christensen

Posts: 5,462
Registered: 7/9/08
Re: Formal Proof of Cantor-Bernstein-Schroeder Theorem using DC Proof 2.0
Posted: Jun 15, 2013 11:44 AM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Jun 15, 2:57 am, Jan Burse <janbu...@fastmail.fm> wrote:
> Dan Christensen schrieb:

> > Full text at:http://dcproof.com/CBS.htm From the informal
> > introduction:

> > THEOREM (Cantor-Bernstein-Schroeder):
> gr8 work! Congratulations.

Thank you.

> The proof has >1000 lines, could it be made shorter?

Currently at 1,262 lines, it could be made a little shorter. I might
be able to get it under 1000. I will be going through the proof at a
later date to see if I can make some improvements.

> When I was googling I found different operators used
> to yield a fixpoint. The one you were using is found
> on the french wikipedia side, another one is shown
> on the german wikipedia side.

I have a proof of the fixed-point theorem as well (241 lines). I hope
to be releasing it, along with a collection of proofs on orders of
infinity, with an update of my program this summer.

Download my DC Proof 2.0 software at http://www.dcproof.com

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2015. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.