Skip to content

Instantly share code, notes, and snippets.

@Nikolaj-K
Last active November 13, 2019 17:29
Show Gist options
  • Save Nikolaj-K/748bb1834f553fc41554144d3161725c to your computer and use it in GitHub Desktop.
Save Nikolaj-K/748bb1834f553fc41554144d3161725c to your computer and use it in GitHub Desktop.
We explicitly proof Cantors theorem

Those are the text used in the video

https://youtu.be/0Sl0bcXyTAo

trivial case

For any finite sets x, we have that |P(x)| > |x|. In particular |{{}}| = |P({})| > |{}|. This is, in terms of Neumann ordinals, 1 > 0. When we say "function" in this text, we always mean function on a non-empty domain.

on function

Consider a theory of sets and a notion of function so that, for each function f, dom(f) is a set. (E.g. when functions are modeled as special relations and relations are sets of pairs in the usual way.)

Definition of "injective":

injective(f) ≡ ∀(x ∈ dom(f)). ∀(y ∈ dom(f)). f(x) = f(y) => x = y

Onto will be defined and used later in this text.

"values are subsets of its domain" predicate V(f)

Consider now the property on functions whos "values are subsets of its domain" V(f) = ∀(x ∈ dom(f)). f(x) ⊆ dom(f)

If the power set P_X exists as a set, we might also say that the values are in the power set. Indeed, then for any set X, consider F: X -> P_X F(x) = {x}

Proposition 1. ∀X. ∃f. V(f) and injective(f)

V(f) functions

For a concrete case, G: N -> P_N G(n) := {n} # always a 1 element set. Also, for the same reason, clearly not onto.

E.g. G(3) = {3} G(10) = {10} But it also works if the codomain is smaller. G': N -> {x | ∃(k ∈ N). x={k} } G'(n) := {n}

Or H: Q -> P_Q H(q) := {q - 1/7, 2 * q} # always a 1 or 2 element set E.g. H(3) = {3 - 1/7, 6} H(1/7) = {0, 2 / 7} H(-1/7) = {-2/7} H(0) := {-1/7, 0}

Or J: N -> P_N J(n) := {k ∈ N | k > 2 * n } E.g. J(10) = {21, 22, 23, ...} J(1) = {3, 4, 5 ...} J(0) = {1, 2, 3, ...} # all members always bigger than 0

Offending set D_F, with examples

Consider for any F with V(f) and the following set, if it exists (very weak assumption) D_F ≡ {x ∈ dom(F) | x ∉ F(x)}

E.g. D_G ≡ {n ∈ N | n ∉ {n}} = {} # is empty D_H ≡ {q ∈ Q | q ∉ {q - 1/7, 9001 * q}} = Q \ {0} # is infinite D_J ≡ {n ∈ N | n ∉ {2n+1, 2n+2,...}} = N # holds the number 0

Note that in those cases at least, the set D_f are all different from the values of F!

Another example

Consider a function I : {3, 5, 9} -> {{5}, D_I} and let's reason about I by considering D_I D_I = {x ∈ {3, 5, 9} | x ∉ I(x)}

For a contradiction, assume I(3) = D_I Then in the comprehension above, 3 ∉ D_I <=> 3 ∈ D_I. As this goes for all n, we find I(n)={5} for all n. Hence D_I = {x ∈ {3, 5, 9} | x ∉ {5}} = {3, 7} So I : {3, 5, 9} -> {{5}, {3, 7}} but D_I is also never taken by D_I as a value.

offending set is offending

Proposition 2: ∄f. V(f) and [ ∃(z ∈ dom(F)). F(z) = D_F ]

For a contradiction, assume ∃f. V(f) and [ ∃(z ∈ dom(F)). F(z) = D_F ] ∃f. V(f) and [ ∃(z ∈ dom(F)). F(z) = {x ∈ dom(F) | x ∉ F(x)} ] ∃f. V(f) and [ ∃z. z ∈ dom(F) and [ ∀x. x ∈ F(z) <=> (x ∈ dom(F) and x ∉ F(x)) ] ]

Take said F and said c ∈ dom(F) and consider the claim ∀x. x ∈ F(c) <=> (x ∈ dom(F) and x ∉ F(x)) Now for a particular, x=c, this then claims c ∈ F(c) <=> (c ∈ dom(F) and c ∉ F(c)) which reduces to c ∈ F(c) <=> c ∉ F(c) A contradiction. QED.

offending set prevents onto

Proposition 3. ∄f. onto(f, P_dom_f)

Let onto(f, Y) ≡ ∀(x ∈ dom(f)). f(x) ∈ Y and ∀(y ∈ Y). ∃(z ∈ dom(f)). f(z) = y

For a contradiction, assume there's a surjection into the power set. I.e., with Y = P_dom_f, ∃f. onto(f, P_dom_f)

Take said F. The first half translates to V(F) and all our above considerations apply.

The second part says ∀(y ∈ P_dom_F). ∃(z ∈ dom(F)). F(z)=y Now for a particular, y=D_F, this then claims ∃(z ∈ dom(F)). F(z)=D_F

Together get get ∃f. V(f) and [ ∃(z ∈ dom(F)). F(z)=D_F ] A contradiction. QED.

classical size hierarchy

We have shown existence of injection and non-existence of surjection, so classically |P_N| > |N|.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment