The Principal of Mathematical Induction derived from the Field Axioms
From the field axioms for the real numbers we construct the set of natural
numbers and derive all but one of Peano's axioms, namely that no natural
number has a successor of 1. We prove that the natural numbers, as constructed
here, uniquely satisfy the remaining axioms.
We begin by constructing the subset n of the reals such that:
Set(n)
& ALL(a):[a ε n <=> a ε real
& ALL(b):[Set(b) & ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> a ε b]]
We prove:
1. ALL(a):[a ε n => a ε real] (Lines 23 to 31)
We suppose that x ε n. Applying the definition of n for x, we immediately obtain obtain x ε real.
Then generalize on x.
2. 1εn (Lines 32 to 43)
Applying the definition of n for 1, we obtain the sufficient conditions for 1 ε n.
Required result then follows trivially.
3. ALL(a):[a ε n => a+1 ε n] (Lines 44 to 74)
Suppose x ε n. Applying the definition of n for a=x and a=x+1, the result follows
trivially.
4. ALL(a):[Set(a) (Lines 75 to 93)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε n => b ε a]]
Suppose the antecedent is true for some set s. Then suppose the x ε n. Applying the definition
of n for x, can easily show that x ε s. Generalize to obtain the required result.
5. EXIST(nat):[Set(nat) & ALL(a):[a ε nat => a ε real] & 1 ε nat (Lines 94 to 98)
& ALL(a):[a ε nat => a+1 ε nat]
& ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε nat => b ε a]]]
Combine previous results and generalize.
5. P(1) (Lines 99 to 162)
& ALL(a):[a ε n & P(a) => P(a+1)]
=> ALL(a):[a ε n => P(a)]
Begin by supposing the antecedent. Then construct subset p of n such that:
ALL(a):[a ε p <=> a ε n & P(a)]
Then apply the principle of mathematical induction (for the reals) from previous result (4) for
set p.
That set p is a subset of the reals, follows from the previous result (1).
1εp follows trivially from the definition of p.
Suppose kεp. Applying the defintion of p for k and k+1, it is easy to show that k+1 ε p.
Generalize this conclusion and the required result follows easily:
ALL(a):[a ε n => P(a)]
6. n=n' given... (Lines 163 to 192)
Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
& ALL(a):[a ε n' => a+1 ε n']
& ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε n' => b ε a]]
Apply PMI in n for set n'. And apply PMI in n' for set n. Result follows trivially.
Field Axioms
************
1 Set(real)
& ALL(a):ALL(b):[a ε real & b ε real => a+b ε real]
& ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a+b+c=a+(b+c)]
& ALL(a):ALL(b):[a ε real & b ε real => a+b=b+a]
& 0 ε real
& ALL(a):[a ε real => a+0=a]
& ALL(a):[a ε real => _a ε real]
& ALL(a):[a ε real => a+_a=0]
& ALL(a):ALL(b):[a ε real & b ε real => a*b ε real]
& ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*b*c=a*(b*c)]
& ALL(a):ALL(b):[a ε real & b ε real => a*b=b*a]
& ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*(b+c)=a*b+a*c]
& 1 ε real
& ~0=1
& ALL(a):[a ε real => a*1=a]
& ALL(a):[a ε real & ~a=0 => 1/a ε real]
& ALL(a):[a ε real => a*(1/a)=1]
Premise
Splitting into individual axioms...
Define: real, the set of real numbers
2 Set(real)
Split, 1
Define: + operator
3 ALL(a):ALL(b):[a ε real & b ε real => a+b ε real]
Split, 1
+ is associative
4 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a+b+c=a+(b+c)]
Split, 1
+ is commutative
5 ALL(a):ALL(b):[a ε real & b ε real => a+b=b+a]
Split, 1
Define: 0
6 0 ε real
Split, 1
7 ALL(a):[a ε real => a+0=a]
Split, 1
Define: _x (additive invervse)
8 ALL(a):[a ε real => _a ε real]
Split, 1
9 ALL(a):[a ε real => a+_a=0]
Split, 1
Define: * operator
10 ALL(a):ALL(b):[a ε real & b ε real => a*b ε real]
Split, 1
* is associative
11 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*b*c=a*(b*c)]
Split, 1
* is commutative
12 ALL(a):ALL(b):[a ε real & b ε real => a*b=b*a]
Split, 1
* is distributive over +
13 ALL(a):ALL(b):ALL(c):[a ε real & b ε real & c ε real => a*(b+c)=a*b+a*c]
Split, 1
Define: 1
14 1 ε real
Split, 1
15 ~0=1
Split, 1
16 ALL(a):[a ε real => a*1=a]
Split, 1
Define: 1/x (multiplicative inverse)
17 ALL(a):[a ε real & ~a=0 => 1/a ε real]
Split, 1
18 ALL(a):[a ε real => a*(1/a)=1]
Split, 1
Construct n
Applying the subset axiom...
19 EXIST(n):[Set(n) & ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> a ε b]]]
Subset, 2
Define: n, the set of natural numbers
20 Set(n) & ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> a ε b]]
E Spec, 19
21 Set(n)
Split, 20
22 ALL(a):[a ε n <=> a ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> a ε b]]
Split, 20
Prove: x ε n => x ε real
Suppose...
23 x ε n
Premise
Apply definition of n for x
24 x ε n <=> x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
U Spec, 22
25 [x ε n => x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]]
& [x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b] => x ε n]
Iff-And, 24
26 x ε n => x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Split, 25
27 x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b] => x ε n
Split, 25
28 x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Detach, 26, 23
29 x ε real
Split, 28
As Required:
30 x ε n => x ε real
Conclusion, 23
As Required:
31 ALL(a):[a ε n => a ε real]
U Gen, 30
Prove: 1 ε n
Apply defintion of n for 1
32 1 ε n <=> 1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b]
U Spec, 22
33 [1 ε n => 1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b]]
& [1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b] => 1 ε n]
Iff-And, 32
34 1 ε n => 1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b]
Split, 33
Sufficient: For 1εn
35 1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b] => 1 ε n
Split, 33
Prove: Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> 1 ε s
Suppose...
36 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
Premise
37 Set(s)
Split, 36
38 ALL(c):[c ε s => c ε real]
Split, 36
39 1 ε s
Split, 36
As Required:
40 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> 1 ε s
Conclusion, 36
Generalizing...
41 ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b]
U Gen, 40
42 1 ε real
& ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> 1 ε b]
Join, 14, 41
As Required:
43 1 ε n
Detach, 35, 42
Prove: xεn => x+1εn
Suppose...
44 x ε n
Premise
Apply definition of n for x
45 x ε n <=> x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
U Spec, 22
46 [x ε n => x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]]
& [x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b] => x ε n]
Iff-And, 45
47 x ε n => x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Split, 46
48 x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b] => x ε n
Split, 46
49 x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Detach, 47, 44
50 x ε real
Split, 49
51 ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Split, 49
Apply definition of n for x+1
52 x+1 ε n <=> x+1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b]
U Spec, 22
53 [x+1 ε n => x+1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b]]
& [x+1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b] => x+1 ε n]
Iff-And, 52
54 x+1 ε n => x+1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b]
Split, 53
Sufficient: For x+1 ε n
55 x+1 ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b] => x+1 ε n
Split, 53
Apply defintion of + for x and 1
56 ALL(b):[x ε real & b ε real => x+b ε real]
U Spec, 3
57 x ε real & 1 ε real => x+1 ε real
U Spec, 56
58 x ε real & 1 ε real
Join, 50, 14
59 x+1 ε real
Detach, 57, 58
Prove: Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> x+1 ε s
Suppose...
60 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
Premise
61 Set(s)
Split, 60
62 ALL(c):[c ε s => c ε real]
Split, 60
63 1 ε s
Split, 60
64 ALL(c):[c ε s => c+1 ε s]
Split, 60
Apply PMI
65 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> x ε s
U Spec, 51
66 x ε s
Detach, 65, 60
Apply defintion of s
67 x ε s => x+1 ε s
U Spec, 64
68 x+1 ε s
Detach, 67, 66
As Required:
69 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> x+1 ε s
Conclusion, 60
Generalizing...
70 ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b]
U Gen, 69
71 x+1 ε real
& ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x+1 ε b]
Join, 59, 70
72 x+1 ε n
Detach, 55, 71
As Required:
73 x ε n => x+1 ε n
Conclusion, 44
As Required:
74 ALL(a):[a ε n => a+1 ε n]
U Gen, 73
Prove: Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> ALL(b):[b ε n => b ε s]
Suppose...
75 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
Premise
76 Set(s)
Split, 75
77 ALL(c):[c ε s => c ε real]
Split, 75
78 1 ε s
Split, 75
79 ALL(c):[c ε s => c+1 ε s]
Split, 75
Prove: xεn => xεs
80 x ε n
Premise
Apply definition of n for x
81 x ε n <=> x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
U Spec, 22
82 [x ε n => x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]]
& [x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b] => x ε n]
Iff-And, 81
83 x ε n => x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Split, 82
84 x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b] => x ε n
Split, 82
85 x ε real & ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Detach, 83, 80
86 x ε real
Split, 85
87 ALL(b):[Set(b)
& ALL(c):[c ε b => c ε real]
& 1 ε b
& ALL(c):[c ε b => c+1 ε b]
=> x ε b]
Split, 85
88 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> x ε s
U Spec, 87
89 x ε s
Detach, 88, 75
As Required:
90 x ε n => x ε s
Conclusion, 80
91 ALL(b):[b ε n => b ε s]
U Gen, 90
As Required:
92 Set(s)
& ALL(c):[c ε s => c ε real]
& 1 ε s
& ALL(c):[c ε s => c+1 ε s]
=> ALL(b):[b ε n => b ε s]
Conclusion, 75
As Required:
93 ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε n => b ε a]]
U Gen, 92
94 Set(n) & ALL(a):[a ε n => a ε real]
Join, 21, 31
95 Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
Join, 94, 43
96 Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
& ALL(a):[a ε n => a+1 ε n]
Join, 95, 74
97 Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
& ALL(a):[a ε n => a+1 ε n]
& ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε n => b ε a]]
Join, 96, 93
98 EXIST(nat):[Set(nat) & ALL(a):[a ε nat => a ε real] & 1 ε nat
& ALL(a):[a ε nat => a+1 ε nat]
& ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε nat => b ε a]]]
E Gen, 97
Prove: P(1)
& ALL(a):[a ε n & P(a) => P(a+1)]
=> ALL(a):[a ε n => P(a)]
Suppose...
99 P(1)
& ALL(a):[a ε n & P(a) => P(a+1)]
Premise
100 P(1)
Split, 99
101 ALL(a):[a ε n & P(a) => P(a+1)]
Split, 99
Apply subset axiom
102 EXIST(p):[Set(p) & ALL(a):[a ε p <=> a ε n & P(a)]]
Subset, 21
Define: p, those natural x numbers for which P(x) is true
103 Set(p) & ALL(a):[a ε p <=> a ε n & P(a)]
E Spec, 102
104 Set(p)
Split, 103
105 ALL(a):[a ε p <=> a ε n & P(a)]
Split, 103
Sufficient: For ALL(b):[b ε n => b ε p]
Apply PMI
106 Set(p)
& ALL(c):[c ε p => c ε real]
& 1 ε p
& ALL(c):[c ε p => c+1 ε p]
=> ALL(b):[b ε n => b ε p]
U Spec, 93
107 1 ε p <=> 1 ε n & P(1)
U Spec, 105
108 [1 ε p => 1 ε n & P(1)] & [1 ε n & P(1) => 1 ε p]
Iff-And, 107
109 1 ε p => 1 ε n & P(1)
Split, 108
110 1 ε n & P(1) => 1 ε p
Split, 108
111 1 ε n & P(1)
Join, 43, 100
As Required:
112 1 ε p
Detach, 110, 111
Prove: kεp => k+1εp
Suppose...
113 k ε p
Premise
Apply definition of p for k
114 k ε p <=> k ε n & P(k)
U Spec, 105
115 [k ε p => k ε n & P(k)] & [k ε n & P(k) => k ε p]
Iff-And, 114
116 k ε p => k ε n & P(k)
Split, 115
117 k ε n & P(k) => k ε p
Split, 115
118 k ε n & P(k)
Detach, 116, 113
119 k ε n
Split, 118
120 P(k)
Split, 118
Apply definition of p for k+1
121 k+1 ε p <=> k+1 ε n & P(k+1)
U Spec, 105
122 [k+1 ε p => k+1 ε n & P(k+1)]
& [k+1 ε n & P(k+1) => k+1 ε p]
Iff-And, 121
123 k+1 ε p => k+1 ε n & P(k+1)
Split, 122
Sufficient: For k+1 ε p
124 k+1 ε n & P(k+1) => k+1 ε p
Split, 122
Apply previous result.
125 k ε n => k+1 ε n
U Spec, 74
126 k+1 ε n
Detach, 125, 119
Apply premise
127 k ε n & P(k) => P(k+1)
U Spec, 101
128 k ε n & P(k)
Join, 119, 120
129 P(k+1)
Detach, 127, 128
130 k+1 ε n & P(k+1)
Join, 126, 129
131 k+1 ε p
Detach, 124, 130
As Required:
132 k ε p => k+1 ε p
Conclusion, 113
As Required:
133 ALL(c):[c ε p => c+1 ε p]
U Gen, 132
Prove: k ε p => k ε real
Suppose...
134 k ε p
Premise
Apply definition of p
135 k ε p <=> k ε n & P(k)
U Spec, 105
136 [k ε p => k ε n & P(k)] & [k ε n & P(k) => k ε p]
Iff-And, 135
137 k ε p => k ε n & P(k)
Split, 136
138 k ε n & P(k) => k ε p
Split, 136
139 k ε n & P(k)
Detach, 137, 134
140 k ε n
Split, 139
141 P(k)
Split, 139
Apply previous result
142 k ε n => k ε real
U Spec, 31
143 k ε real
Detach, 142, 140
As Required:
144 k ε p => k ε real
Conclusion, 134
As Required:
145 ALL(c):[c ε p => c ε real]
U Gen, 144
146 Set(p) & ALL(c):[c ε p => c ε real]
Join, 104, 145
147 Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p
Join, 146, 112
148 Set(p) & ALL(c):[c ε p => c ε real] & 1 ε p
& ALL(c):[c ε p => c+1 ε p]
Join, 147, 133
As Required:
149 ALL(b):[b ε n => b ε p]
Detach, 106, 148
Prove: k ε n => P(k)
Suppose...
150 k ε n
Premise
151 k ε n => k ε p
U Spec, 149
152 k ε p
Detach, 151, 150
153 k ε p <=> k ε n & P(k)
U Spec, 105
154 [k ε p => k ε n & P(k)] & [k ε n & P(k) => k ε p]
Iff-And, 153
155 k ε p => k ε n & P(k)
Split, 154
156 k ε n & P(k) => k ε p
Split, 154
157 k ε n & P(k)
Detach, 155, 152
158 k ε n
Split, 157
159 P(k)
Split, 157
As Required:
160 k ε n => P(k)
Conclusion, 150
Generalizing...
161 ALL(a):[a ε n => P(a)]
U Gen, 160
As Required:
162 P(1)
& ALL(a):[a ε n & P(a) => P(a+1)]
=> ALL(a):[a ε n => P(a)]
Conclusion, 99
Prove: n=n' given...
163 Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
& ALL(a):[a ε n' => a+1 ε n']
& ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε n' => b ε a]]
E Spec, 98
164 Set(n')
Split, 163
165 ALL(a):[a ε n' => a ε real]
Split, 163
166 1 ε n'
Split, 163
167 ALL(a):[a ε n' => a+1 ε n']
Split, 163
168 ALL(a):[Set(a)
& ALL(c):[c ε a => c ε real]
& 1 ε a
& ALL(c):[c ε a => c+1 ε a]
=> ALL(b):[b ε n' => b ε a]]
Split, 163
169 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c ε a <=> c ε b]]]
Set Equality
170 ALL(b):[Set(n) & Set(b) => [n=b <=> ALL(c):[c ε n <=> c ε b]]]
U Spec, 169
171 Set(n) & Set(n') => [n=n' <=> ALL(c):[c ε n <=> c ε n']]
U Spec, 170
172 Set(n) & Set(n')
Join, 21, 164
173 n=n' <=> ALL(c):[c ε n <=> c ε n']
Detach, 171, 172
174 [n=n' => ALL(c):[c ε n <=> c ε n']]
& [ALL(c):[c ε n <=> c ε n'] => n=n']
Iff-And, 173
175 n=n' => ALL(c):[c ε n <=> c ε n']
Split, 174
Sufficient: For n=n'
176 ALL(c):[c ε n <=> c ε n'] => n=n'
Split, 174
Apply PMI in n
177 Set(n')
& ALL(c):[c ε n' => c ε real]
& 1 ε n'
& ALL(c):[c ε n' => c+1 ε n']
=> ALL(b):[b ε n => b ε n']
U Spec, 93
178 Set(n') & ALL(a):[a ε n' => a ε real]
Join, 164, 165
179 Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
Join, 178, 166
180 Set(n') & ALL(a):[a ε n' => a ε real] & 1 ε n'
& ALL(a):[a ε n' => a+1 ε n']
Join, 179, 167
181 ALL(b):[b ε n => b ε n']
Detach, 177, 180
Apply PMI in n'
182 Set(n)
& ALL(c):[c ε n => c ε real]
& 1 ε n
& ALL(c):[c ε n => c+1 ε n]
=> ALL(b):[b ε n' => b ε n]
U Spec, 168
183 Set(n) & ALL(a):[a ε n => a ε real]
Join, 21, 31
184 Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
Join, 183, 43
185 Set(n) & ALL(a):[a ε n => a ε real] & 1 ε n
& ALL(a):[a ε n => a+1 ε n]
Join, 184, 74
186 ALL(b):[b ε n' => b ε n]
Detach, 182, 185
187 k ε n => k ε n'
U Spec, 181
188 k ε n' => k ε n
U Spec, 186
189 [k ε n => k ε n'] & [k ε n' => k ε n]
Join, 187, 188
190 k ε n <=> k ε n'
Iff-And, 189
191 ALL(a):[a ε n <=> a ε n']
U Gen, 190
As Required:
The subset n uniquely satisfies the remaining Peano Axioms?????
192 n=n'
Detach, 176, 191