Skip to content

Formal Proof of the Cantor-Bernstein-Schroeder Theorem

June 24, 2013
File:Georg Cantor2.jpg

Georg Cantor
1845 – 1918

The Cantor-Bernstein-Schroeder Theorem (CBST), is one of the most important and widely applied results in set theory:

If set X can be mapped one-to-one into set Y (an injection), and set Y can be mapped one-to-one into set X (an injection), then X can be mapped one-to-one onto Y (a bijection).

Though seemingly self-evident, some proofs of  CBST can make your head spin! Every line of my machine-verified, formal proof (updated 2014-09-11) is justified by one of a very limited list of simple axioms and rules of inference (indicated in a grey font at the end of each line).

Such complete rigour does come at a price, however. While it is completely free of any of the sort of the hand-waving that plagues many informal versions of this proof, like most formal proofs of any complexity, it is very long. My commentary (indicated by a blue font) is inserted throughout using DC Proof. I believe this makes my proof considerably more readable than machine-generated formal proofs in other systems.

This proof was written to demonstrate he capabilities of the DC Proof system. Though designed for ease of use by the complete beginner, DC Proof is quite capable of some mathematical heavy lifting.


From → Uncategorized

Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: