THEOREM
*******
Given the existence of a
Dedekind infinite set, there exists a subset of it on which Peano's
Axioms hold.
EXIST(n):EXIST(s):EXIST(0):[
0 e n
PA1
& ALL(a):[a e n => s(a) e n] PA2
& ALL(a):ALL(b):[a
e n & b e n =>
[s(a)=s(b) => a=b]] PA3
& ALL(a):[a e n => ~s(a)=0] PA4
& ALL(p):[Set(p)
& ALL(c):[c e p => c e n] PA5 (Induction)
=> [0 e p &
ALL(c):[c e p => s(c) e p]
=> ALL(a):[a e n => a e p]]]]
Dan Christensen
2023-02-19
http://www.dcproof.com
PROOF
*****
Let x be a Dedekind infinite
set, i.e. there exists on it a function f that is
injective
and not
surjective.
1 Set(x)
Axiom
f is a function
mapping x to itself
2 ALL(a):[a e x => f(a) e x]
Axiom
f is injective
3 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
Axiom
f is not
surjective
4 ~ALL(a):[a e x =>
EXIST(b):[b e x & f(b)=a]]
Axiom
Change quanitifier,
etc.
5 ~~EXIST(a):~[a e x =>
EXIST(b):[b e x & f(b)=a]]
Quant, 4
6 EXIST(a):~[a e x => EXIST(b):[b e x & f(b)=a]]
Rem DNeg, 5
7 EXIST(a):~~[a e x & ~EXIST(b):[b e x & f(b)=a]]
Imply-And, 6
8 EXIST(a):[a e x & ~EXIST(b):[b e x & f(b)=a]]
Rem DNeg, 7
9 EXIST(a):[a e x & ~~ALL(b):~[b e x & f(b)=a]]
Quant, 8
10 EXIST(a):[a e x & ALL(b):~[b e x & f(b)=a]]
Rem DNeg, 9
11 EXIST(a):[a e x & ALL(b):~~[b e x => ~f(b)=a]]
Imply-And, 10
12 EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
Rem DNeg, 11
13 x0 e x & ALL(b):[b e x => ~f(b)=x0]
E Spec, 12
As Required:
14 x0 e x
Split, 13
15 ALL(b):[b e x => ~f(b)=x0]
Split, 13
Apply Subset Axiom
16 EXIST(sub):[Set(sub)
& ALL(a):[a e sub <=> a e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]]
Subset, 1
17 Set(n) & ALL(a):[a e n <=> a e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]
E Spec, 16
Define: n
18 Set(n)
Split, 17
19 ALL(a):[a e n <=> a e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]
Split, 17
Prove: ALL(a):[a e n => a e x]
Suppose...
20 t e n
Premise
21 t e n <=> t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
U Spec, 19
22 [t e n => t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]]
&
[t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b] => t e n]
Iff-And, 21
23 t e n => t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Split, 22
24 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Detach, 23, 20
25 t e x
Split, 24
n is a subset
of x
26 ALL(a):[a e n => a e x]
4 Conclusion, 20
Apply definition of n
27 x0 e n <=> x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]
U Spec, 19
28 [x0 e n => x0 e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b]]
&
[x0 e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b] => x0 e n]
Iff-And, 27
Sufficient: For x0 e n
29 x0 e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => x0 e b] => x0 e n
Split, 28
Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
Suppose...
30 Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
Premise
31 x0 e b
Split, 30
As Required:
32 ALL(b):[Set(b) &
ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
=>
x0 e b]
4 Conclusion, 30
33 x0 e x
&
ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
=>
x0 e b]
Join, 14, 32
PA1:
----
34 x0 e n
Detach, 29, 33
Prove: ALL(a):[a e n => f(a) e n]
Suppose...
35 t e n
Premise
Apply definition of n
36 t e n <=> t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
U Spec, 19
37 [t e n => t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]]
&
[t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b] => t e n]
Iff-And, 36
38 t e n => t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Split, 37
39 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Detach, 38, 35
40 t e x
Split, 39
41 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Split, 39
Apply Axiom
42 t e x => f(t) e x
U Spec, 2
43 f(t) e x
Detach, 42, 40
Apply definition of n
44 f(t) e n <=> f(t) e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) e b]
U Spec, 19, 43
45 [f(t) e n => f(t) e x &
ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) e b]]
&
[f(t) e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) e b] => f(t) e n]
Iff-And, 44
Sufficient: For f(t) e n
46 f(t) e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) e b] => f(t) e n
Split, 45
Prove: ALL(b):[Set(b) &
ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
=> f(t) e b]
Suppose...
47 Set(u) & ALL(c):[c e u => c e x] & x0 e u & ALL(c):[c e u => f(c) e u]
Premise
48 Set(u)
Split, 47
49 ALL(c):[c e u => c e x]
Split, 47
50 x0 e u
Split, 47
51 ALL(c):[c e u => f(c) e u]
Split, 47
52 Set(u) & ALL(c):[c e u => c e x] & x0 e u & ALL(c):[c e u => f(c) e u] => t e u
U Spec, 41
53 t e u
Detach, 52, 47
54 t e u => f(t) e u
U Spec, 51
55 f(t) e u
Detach, 54, 53
As Required:
56 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
=>
f(t) e b]
4 Conclusion, 47
57 f(t) e x
&
ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]
=>
f(t) e b]
Join, 43, 56
58 f(t) e n
Detach, 46, 57
PA2:
----
59 ALL(a):[a e n => f(a) e n]
4 Conclusion, 35
Prove: ALL(a):ALL(b):[a e n & b e n =>
[f(a)=f(b) => a=b]]
Suppose...
60 t e n & u e n
Premise
61 t e n
Split, 60
62 u e n
Split, 60
63 ALL(b):[t e x & b e x => [f(t)=f(b) => t=b]]
U Spec, 3
64 t e x & u e x => [f(t)=f(u) => t=u]
U Spec, 63
65 t e n => t e x
U Spec, 26
66 t e x
Detach, 65, 61
67 u e n => u e x
U Spec, 26
68 u e x
Detach, 67, 62
69 t e x & u e x
Join, 66, 68
70 f(t)=f(u) => t=u
Detach, 64, 69
PA3:
----
71 ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
4 Conclusion, 60
Prove: ALL(a):[a e n => ~f(a)=x0]
Suppose...
72 t e n
Premise
73 t e x => ~f(t)=x0
U Spec, 15
74 t e n => t e x
U Spec, 26
75 t e x
Detach, 74, 72
76 ~f(t)=x0
Detach, 73, 75
PA4:
----
77 ALL(a):[a e n => ~f(a)=x0]
4 Conclusion, 72
Prove: ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=> [x0 e p & ALL(c):[c e p => f(c) e p]
=> ALL(a):[a e n => a e p]]]
Suppose p is a subset of n
78 Set(p) & ALL(c):[c e p => c e n]
Premise
Prove: x0 e p &
ALL(c):[c e p => f(c) e p]
=> ALL(a):[a e n => a e p]
Suppose...
79 x0 e p & ALL(c):[c e p => f(c) e p]
Premise
80 Set(p)
Split, 78
81 ALL(c):[c e p => c e n]
Split, 78
82 x0 e p
Split, 79
83 ALL(c):[c e p => f(c) e p]
Split, 79
Prove: ALL(b):[b e n => b e p]
Suppose...
84 t e n
Premise
85 t e n <=> t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
U Spec, 19
86 [t e n => t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]]
&
[t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b] => t e n]
Iff-And, 85
87 t e n => t e x & ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Split, 86
88 t e x & ALL(b):[Set(b)
& ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Detach, 87, 84
89 t e x
Split, 88
90 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]
Split, 88
Sufficient: For t e p
91 Set(p) & ALL(c):[c e p => c e x] & x0 e p & ALL(c):[c e p => f(c) e p] => t e p
U Spec, 90
Prove: ALL(a):[a e n => a e p]
Suppose...
92 u e p
Premise
93 u e p => u e n
U Spec, 81
94 u e n
Detach, 93, 92
95 u e n => u e x
U Spec, 26
96 u e x
Detach, 95, 94
As Required:
97 ALL(c):[c e p => c e x]
4 Conclusion, 92
98 Set(p) & ALL(c):[c e p => c e x]
Join, 80, 97
99 Set(p) & ALL(c):[c e p => c e x] & x0 e p
Join, 98, 82
100 Set(p) & ALL(c):[c e p => c e x] & x0 e p
&
ALL(c):[c e p => f(c) e p]
Join, 99, 83
101 t e p
Detach, 91, 100
As Required:
102 ALL(a):[a e n => a e p]
4 Conclusion, 84
As Required:
103 x0 e p & ALL(c):[c e p => f(c) e p]
=>
ALL(a):[a e n => a e p]
4 Conclusion, 79
PA5:
----
104 ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=>
[x0 e p & ALL(c):[c e p => f(c) e p]
=>
ALL(a):[a e n => a e p]]]
4 Conclusion, 78
105 x0 e n & ALL(a):[a e n => f(a) e n]
Join, 34, 59
106 x0 e n & ALL(a):[a e n => f(a) e n]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
Join, 105, 71
107 x0 e n & ALL(a):[a e n => f(a) e n]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
&
ALL(a):[a e n => ~f(a)=x0]
Join, 106, 77
108 x0 e n & ALL(a):[a e n => f(a) e n]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
&
ALL(a):[a e n => ~f(a)=x0]
&
ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=>
[x0 e p & ALL(c):[c e p => f(c) e p]
=>
ALL(a):[a e n => a e p]]]
Join, 107, 104
109 EXIST(0):[0 e n & ALL(a):[a e n => f(a) e n]
&
ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]]
&
ALL(a):[a e n => ~f(a)=0]
&
ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=>
[0 e p & ALL(c):[c e p => f(c) e p]
=>
ALL(a):[a e n => a e p]]]]
E Gen, 108
110 EXIST(s):EXIST(0):[0 e n & ALL(a):[a e n => s(a) e n]
&
ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
&
ALL(a):[a e n => ~s(a)=0]
&
ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=>
[0 e p & ALL(c):[c e p => s(c) e p]
=>
ALL(a):[a e n => a e p]]]]
E Gen, 109
As Required:
111 EXIST(n):EXIST(s):EXIST(0):[0 e n &
ALL(a):[a e n => s(a) e n]
&
ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
&
ALL(a):[a e n => ~s(a)=0]
&
ALL(p):[Set(p) & ALL(c):[c e p => c e n]
=>
[0 e p & ALL(c):[c e p => s(c) e p]
=>
ALL(a):[a e n => a e p]]]]
E Gen, 110