THEOREM
*******
As a consequence of the proposed Axiom of Infinity, there exists a set n that satifies
the Peano Axioms
EXIST(n):EXIST(next):EXIST(n0):[Set(n)
& n0 e n PA1
& ALL(a):[a e n => next(a) e n] PA2
& ALL(b):ALL(c):[b e n & c e n => [next(b)=next(c) => b=c]] PA3
& ALL(b):[b e n => ~next(b)=n0] PA4
& ALL(b):[Set(b) PA5
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e n => c e b]]]
By Dan Christensen
2014-02-02
This proof was written with the aid of the author's DC Proof 2.0 software available free
Proposed Axiom of Infinity
**************************
There exists a set on which an injective, but not surjective function is defined.
1 EXIST(a):EXIST(f):[Set(a)
& ALL(b):[b e a => f(b) e a]
& ALL(b):ALL(c):[b e a & c e a => [f(b)=f(c) => b=c]]
& EXIST(b):[b e a & ALL(c):[c e a => ~f(c)=b]]]
Axiom
Apply Axiom of Infinity
2 EXIST(f):[Set(s)
& ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]]
E Spec, 1
3 Set(s)
& ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
& EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]
E Spec, 2
Define: s, f
************
s is a set
4 Set(s)
Split, 3
f is a function mapping s to itself
5 ALL(b):[b e s => f(b) e s]
Split, 3
f is injective (1-to-1)
6 ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
Split, 3
f is not surjective (not onto)
7 EXIST(b):[b e s & ALL(c):[c e s => ~f(c)=b]]
Split, 3
8 s0 e s & ALL(c):[c e s => ~f(c)=s0]
E Spec, 7
Define: s0, an element of s with no pre-image under f
9 s0 e s
Split, 8
10 ALL(c):[c e s => ~f(c)=s0]
Split, 8
Apply Subset Axiom
11 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]]
Subset, 4
12 Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]
E Spec, 11
Define: n
*********
A subset of s
13 Set(n)
Split, 12
14 ALL(a):[a e n <=> a e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]
Split, 12
Prove: s0 e n
Apply definition of n
15 s0 e n <=> s0 e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b]
U Spec, 14
16 [s0 e n => s0 e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b]]
& [s0 e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b] => s0 e n]
Iff-And, 15
17 s0 e n => s0 e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b]
Split, 16
Sufficient: s0 e n
18 s0 e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b] => s0 e n
Split, 16
Prove: ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b]
Suppose...
19 Set(x)
& s0 e x
& ALL(c):[c e x & c e s => f(c) e x]
Premise
20 Set(x)
Split, 19
21 s0 e x
Split, 19
As Required:
22 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b]
4 Conclusion, 19
23 s0 e s
& ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s0 e b]
Join, 9, 22
PA1
***
24 s0 e n
Detach, 18, 23
Prove: ALL(b):[b e n => f(b) e n]
Suppose...
25 x e n
Premise
Apply definition n
26 x e n <=> x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 14
27 [x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 26
28 x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 27
29 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 27
30 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 28, 25
31 x e s
Split, 30
32 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 30
Apply definition of n
33 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
U Spec, 14
34 [f(x) e n => f(x) e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]]
& [f(x) e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b] => f(x) e n]
Iff-And, 33
35 f(x) e n => f(x) e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Split, 34
Sufficient: For f(x) e n
36 f(x) e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b] => f(x) e n
Split, 34
Apply definition of s, f
37 x e s => f(x) e s
U Spec, 5
38 f(x) e s
Detach, 37, 31
Prove: ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Suppose...
39 Set(p)
& s0 e p
& ALL(c):[c e p & c e s => f(c) e p]
Premise
40 Set(p)
Split, 39
41 s0 e p
Split, 39
42 ALL(c):[c e p & c e s => f(c) e p]
Split, 39
From definition of n...
43 Set(p)
& s0 e p
& ALL(c):[c e p & c e s => f(c) e p]
=> x e p
U Spec, 32
44 x e p
Detach, 43, 39
45 x e p & x e s => f(x) e p
U Spec, 42
46 x e p & x e s
Join, 44, 31
47 f(x) e p
Detach, 45, 46
As Required:
48 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
4 Conclusion, 39
49 f(x) e s
& ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Join, 38, 48
50 f(x) e n
Detach, 36, 49
PA2
***
51 ALL(a):[a e n => f(a) e n]
4 Conclusion, 25
Prove: ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
Suppose...
52 x e n & y e n
Premise
53 x e n
Split, 52
54 y e n
Split, 52
From definition of s, f...
55 ALL(c):[x e s & c e s => [f(x)=f(c) => x=c]]
U Spec, 6
Sufficient: For f(x)=f(y) => x=y
56 x e s & y e s => [f(x)=f(y) => x=y]
U Spec, 55
Prove: x e s
Apply definition of n
57 x e n <=> x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 14
58 [x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 57
59 x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 58
60 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 58
61 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 59, 53
As Required:
62 x e s
Split, 61
63 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 61
Prove: y e s
Apply definition of n
64 y e n <=> y e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
U Spec, 14
65 [y e n => y e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]]
& [y e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b] => y e n]
Iff-And, 64
66 y e n => y e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
Split, 65
67 y e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b] => y e n
Split, 65
68 y e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
Detach, 66, 54
As Required:
69 y e s
Split, 68
70 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
Split, 68
71 x e s & y e s
Join, 62, 69
72 f(x)=f(y) => x=y
Detach, 56, 71
PA3
***
73 ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
4 Conclusion, 52
Prove: ALL(b):[b e n => ~f(b)=s0]
Suppose...
74 x e n
Premise
Apply definition of s, f
75 x e s => ~f(x)=s0
U Spec, 10
Prove: x e s
Apply definition of n
76 x e n <=> x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 14
77 [x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 76
78 x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 77
79 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 77
80 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 78, 74
As Required:
81 x e s
Split, 80
82 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 80
83 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 78, 74
84 ~f(x)=s0
Detach, 75, 81
PA4
***
85 ALL(b):[b e n => ~f(b)=s0]
4 Conclusion, 74
Prove: ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
Suppose...
86 Set(p)
& ALL(c):[c e p => c e n]
& s0 e p
& ALL(c):[c e p => f(c) e p]
Premise
87 Set(p)
Split, 86
88 ALL(c):[c e p => c e n]
Split, 86
89 s0 e p
Split, 86
90 ALL(c):[c e p => f(c) e p]
Split, 86
Prove: ALL(c):[c e n => c e p]
Suppose...
91 x e n
Premise
Apply definition of n
92 x e n <=> x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 14
93 [x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 92
94 x e n => x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 93
95 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 93
96 x e s & ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 94, 91
97 x e s
Split, 96
98 ALL(b):[Set(b)
& s0 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 96
Sufficient: x e p
99 Set(p)
& s0 e p
& ALL(c):[c e p & c e s => f(c) e p]
=> x e p
U Spec, 98
100 y e p & y e s
Premise
101 y e p
Split, 100
102 y e s
Split, 100
Apply previous result
103 y e p => f(y) e p
U Spec, 90
104 f(y) e p
Detach, 103, 101
As Required:
105 ALL(c):[c e p & c e s => f(c) e p]
4 Conclusion, 100
106 Set(p) & s0 e p
Join, 87, 89
107 Set(p) & s0 e p
& ALL(c):[c e p & c e s => f(c) e p]
Join, 106, 105
108 x e p
Detach, 99, 107
As Required:
109 ALL(c):[c e n => c e p]
4 Conclusion, 91
PA5
***
110 ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
4 Conclusion, 86
Joining results...
111 Set(n)
& s0 e n
Join, 13, 24
112 Set(n)
& s0 e n
& ALL(a):[a e n => f(a) e n]
Join, 111, 51
113 Set(n)
& s0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
Join, 112, 73
114 Set(n)
& s0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s0]
Join, 113, 85
115 Set(n)
& s0 e n
& ALL(a):[a e n => f(a) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
Join, 114, 110
Generalizing...
116 EXIST(n0):[Set(n) & n0 e n & ALL(a):[a e n => f(a) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=n0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]]
E Gen, 115
117 EXIST(next):EXIST(n0):[Set(n)
& n0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(b):ALL(c):[b e n & c e n => [next(b)=next(c) => b=c]]
& ALL(b):[b e n => ~nextb)=n0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e n => c e b]]]
E Gen, 116
As Required:
118 EXIST(n):EXIST(next):EXIST(n0):[Set(n)
& n0 e n
& ALL(a):[a e n => next(a) e n]
& ALL(b):ALL(c):[b e n & c e n => [next(b)=next(c) => b=c]]
& ALL(b):[b e n => ~next(b)=n0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& n0 e b
& ALL(c):[c e b => next(c) e b]
=> ALL(c):[c e n => c e b]]]
E Gen, 117