Cantor's Theorem
Theorem: For any set (finite or otherwise), there exists an even larger set.
Prove: ALL(s):[Set(s)
=> EXIST(s'):[Set(s')
& ~EXIST(f):[ALL(a):[a
s => f(a)s'] & ALL(a):[as' => EXIST(b):[bs & a=f(b)]]]]]
Here, a set s' is said to be larger than a set s if there can be no function
mapping s onto all of s'.
Prove: Set(s)
=> EXIST(s'):[Set(s')
& ~EXIST(f):[ALL(a):[as => f(a)s'] & ALL(a):[as' => EXIST(b):[bs & a=f(b)]]]]
Suppose...
1 Set(s)
Premise
Construct the power set of s. We will show that it must be larger than s.
Applying the Power Set Axiom...
2 ALL(a):[Set(a) => EXIST(b):[Set(b)
& ALL(c):[cb <=> Set(c) & ALL(d):[dc => da]]]]
Power Set
3 Set(s) => EXIST(b):[Set(b)
& ALL(c):[cb <=> Set(c) & ALL(d):[dc => ds]]]
U Spec, 2
Applying the Detachment Rule on lines 3 and 1...
4 EXIST(b):[Set(b)
& ALL(c):[cb <=> Set(c) & ALL(d):[dc => ds]]]
Detach, 3, 1
Define: p, the power set of s
5 Set(p)
& ALL(c):[cp <=> Set(c) & ALL(d):[dc => ds]]
E Spec, 4
Splitting this definition into its component parts...
6 Set(p)
Split, 5
7 ALL(c):[cp <=> Set(c) & ALL(d):[dc => ds]]
Split, 5
Prove: There is no f function mapping s onto all of p, that is
~[ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]]
Suppose to the contrary...
8 ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]
Premise
Splitting this premise...
9 ALL(a):[as => f(a)p]
Split, 8
10 ALL(a):[ap => EXIST(b):[bs & a=f(b)]]
Split, 8
Construct k, a subset of s to obtain a contradiction.
Applying the Subset Axiom...
11 EXIST(k):[Set(k) & ALL(a):[ak <=> as & ~af(a)]]
Subset, 1
Define: k, a subset of s
12 Set(k) & ALL(a):[ak <=> as & ~af(a)]
E Spec, 11
Splitting this definition...
13 Set(k)
Split, 12
14 ALL(a):[ak <=> as & ~af(a)]
Split, 12
Prove: kp
Applying the definition of p (the power set of s)...
15 kp <=> Set(k) & ALL(d):[dk => ds]
U Spec, 7
Splitting this IFF-statement into it component implications...
16 [kp => Set(k) & ALL(d):[dk => ds]]
& [Set(k) & ALL(d):[dk => ds] => kp]
Iff-And, 15
Splitting this AND-statement into its component parts...
17 kp => Set(k) & ALL(d):[dk => ds]
Split, 16
Sufficient: For kp
18 Set(k) & ALL(d):[dk => ds] => kp
Split, 16
Prove: xk => xs
Suppose...
19 xk
Premise
Applying the definition of k...
20 xk <=> xs & ~xf(x)
U Spec, 14
Splitting this IFF-statement into its component parts...
21 [xk => xs & ~xf(x)] & [xs & ~xf(x) => xk]
Iff-And, 20
Splitting this AND-statement into its component parts...
22 xk => xs & ~xf(x)
Split, 21
23 xs & ~xf(x) => xk
Split, 21
Applying the Detachment Rule on lines 22 and 19...
24 xs & ~xf(x)
Detach, 22, 19
Splitting this result and deleting the second part...
25 xs
Split, 24
Applying the Conclusion Rule...
26 xk => xs
Conclusion, 19
Generalizing...
27 ALL(d):[dk => ds]
U Gen, 26
28 Set(k) & ALL(d):[dk => ds]
Join, 13, 27
As Required:
29 kp
Detach, 18, 28
Obtain the pre-image of k. Applying the definition of f...
30 kp => EXIST(b):[bs & k=f(b)]
U Spec, 10
Applying the Detachment Rule on lines 30 and 29...
31 EXIST(b):[bs & k=f(b)]
Detach, 30, 29
Define: k', the pre-image of k under f
32 k's & k=f(k')
E Spec, 31
Splitting this result...
33 k's
Split, 32
34 k=f(k')
Split, 32
Is k'k? Applying the definition of k...
35 k'k <=> k's & ~k'f(k')
U Spec, 14
Substituting...
36 k'k <=> k's & ~k'k
Substitute, 34, 35
Splitting this IFF-statement into its component parts...
37 [k'k => k's & ~k'k] & [k's & ~k'k => k'k]
Iff-And, 36
Splitting this AND-statement...
38 k'k => k's & ~k'k
Split, 37
39 k's & ~k'k => k'k
Split, 37
Prove: ~k'k
Suppose to the contrary...
40 k'k
Premise
From the definition of k...
41 k's & ~k'k
Detach, 38, 40
Splitting this result...
42 k's
Split, 41
As Required:
43 ~k'k
Split, 41
We obtain the contradiction...
44 k'k & ~k'k
Join, 40, 43
Applying the Conclusion Rule, by contradiction...
45 ~k'k
Conclusion, 40
Joining previous results...
46 k's & ~k'k
Join, 33, 45
From the definition of k, we also have...
47 k'k
Detach, 39, 46
Joining results, we obtain the contradiction...
48 ~k'k & k'k
Join, 45, 47
Applying the Conclusion Rule, by contradiction...
49 ~[ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]]
Conclusion, 8
Generalizing...
50 ALL(f):~[ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]]
U Gen, 49
Switching quantifiers...
51 ~EXIST(f):~~[ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]]
Quant, 50
Removing the double negation...
52 ~EXIST(f):[ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]]
Rem DNeg, 51
Joining results on lines 6 and 52...
53 Set(p)
& ~EXIST(f):[ALL(a):[as => f(a)p] & ALL(a):[ap => EXIST(b):[bs & a=f(b)]]]
Join, 6, 52
As Required:
Generalizing, we have...
54 EXIST(s'):[Set(s')
& ~EXIST(f):[ALL(a):[as => f(a)s'] & ALL(a):[as' => EXIST(b):[bs & a=f(b)]]]]
E Gen, 53
Applying the Conclusion Rule...
55 Set(s)
=> EXIST(s'):[Set(s')
& ~EXIST(f):[ALL(a):[as => f(a)s'] & ALL(a):[as' => EXIST(b):[bs & a=f(b)]]]]
Conclusion, 1
As Required:
Generalizing...
56 ALL(s):[Set(s)
=> EXIST(s'):[Set(s')
& ~EXIST(f):[ALL(a):[as => f(a)s'] & ALL(a):[as' => EXIST(b):[bs & a=f(b)]]]]]
U Gen, 55