Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.


Math Forum
»
Discussions
»
sci.math.*
»
sci.math
Notice: We are no longer accepting new posts, but the forums will continue to be readable.
Topic:
Formal Proof of CantorBernsteinSchroeder Theorem using DC Proof 2.0
Replies:
2
Last Post:
Jun 15, 2013 11:44 AM




Formal Proof of CantorBernsteinSchroeder Theorem using DC Proof 2.0
Posted:
Jun 14, 2013 11:08 AM


Full text at: http://dcproof.com/CBS.htm From the informal introduction:
THEOREM (CantorBernsteinSchroeder):
Suppose we have sets x and y, and injections f: x > y and g: y > x
Set(x) (x is a set) & Set(y) (y is a set) & ALL(a):[a e x => f(a) e y] (f: x > y) & ALL(a):[a e y => g(a) e x] (g: y > x) & Injection(f,x,y) (f is an injection) & Injection(g,y,x) (g is an injection)
then there exists bijection k: x > y
ALL(a):[a e x => k(a) e y] (k: x > y) & Bijection(k,x,y) (k is a bijection)
where e = epsilon (set membership)
OUTLINE:
We start with sets x and y, injections f: x > y and g: y > x
From these, we construct, using the axioms of set theory and previously established lemmas, various sets and functions that will be required:
px = the power set of x py = the power set of y px2 = the Cartesian prouduct of px with itself xy = the Cartesian prouduct of x and y imgF(s) = the image of s under f imgG(s) = the image of s under g cx(s) = the complement of s relative to x cy(s) = the complement of s relative to y h(s) = cx(imgG(cy(imgF(s)))) g' = the inverse of a suitable restriction (subset) of g
Then we prove that for subsets s1 and s1 of x, if s1 is a subset of s2, then h(s1) is also a subset of h(s2). We say that h is increasing.
Using the KnasterTarski FixedPoint Lemma, we establish the existence of a subset z of x such h(z)=z.
Then we construct the function k: x > y such that
k(a) = f(a) if a e z = g'(a) otherwise
Finally, we prove that k is required bijection.
Dan Download my DC Proof 2.0 software at http://www.dcproof.com



