Search All of the Math Forum:

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

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

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

 Messages: [ Previous | Next ]
 Dan Christensen Posts: 8,219 Registered: 7/9/08
Formal Proof of Cantor-Bernstein-Schroeder 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 (Cantor-Bernstein-Schroeder):

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 Knaster-Tarski Fixed-Point 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