Constructing the Natural Numbers from the Reals
From the field and order axioms for the real numbers, we show here that there
exists a unique subset n in the set of real numbers such that:
1 
n
& ALL(a):[a n => a+1 n]
& ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
& ALL(a):[a n => ~a+1=1]
& ALL(s):[Set(s)
& ALL(c):[c s => c real] & 1 s & ALL(c):[c s => c+1 s]
=> ALL(a):[a n => a s]]
These properties correspond to Peano's Axioms for the natural numbers.
(F5 for overview)
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
Order Axioms
************
19 Set(pos)
& ALL(a):[a pos => a real]
& ALL(a):[a real
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
& ALL(a):ALL(b):[a real & b real & a pos & b pos => a+b pos]
& ALL(a):ALL(b):[a real & b real & a pos & b pos => a*b pos]
& ALL(a):ALL(b):[a real & b real => [a<b <=> b+_a pos]]
& ALL(a):ALL(b):[a real & b real => [a<=b <=> a<b | a=b]]
Premise
Splitting into individual axioms...
Define: pos, the set of postive elements of the set real
20 Set(pos)
Split, 19
pos is a subset of real
21 ALL(a):[a pos => a real]
Split, 19
The Trichotomy Rule
22 ALL(a):[a real
=> [a=0 | a pos | _a pos]
& ~[a=0 & a pos]
& ~[a=0 & _a pos]
& ~[a pos & _a pos]]
Split, 19
Adding postive elements
23 ALL(a):ALL(b):[a real & b real & a pos & b pos => a+b pos]
Split, 19
Mulitplying postive elements
24 ALL(a):ALL(b):[a real & b real & a pos & b pos => a*b pos]
Split, 19
Define: < relation
25 ALL(a):ALL(b):[a real & b real => [a<b <=> b+_a pos]]
Split, 19
Define: <= relation
26 ALL(a):ALL(b):[a real & b real => [a<=b <=> a<b | a=b]]
Split, 19
Previously established results
******************************
Lemma 1
27 0<1
Premise
Lemma 2 Additivity of <
28 ALL(a):ALL(b):ALL(c):[a real & b real & c real & a<b => a+c<b+c]
Premise
Lemma 3 Transitivity of <
29 ALL(a):ALL(b):ALL(c):[a real & b real & c real & a<b & b<c => a<c]
Premise
Lemma 4 Right cancellation, and adding same to both sides
30 ALL(a):ALL(b):ALL(c):[a real & b real & c real => [a=b <=> a+c=b+c]]
Premise
Lemma 5
31 _1 real
Premise
Lemma 6
32 _0=0
Premise
Lemma 7 x+1=y => x<y
33 ALL(a):ALL(b):[a real & b real & a+1=b => a<b]
Premise
Lemma 8 x<=y <=> ~y<x
34 ALL(a):ALL(b):[a real & b real => [a<=b <=> ~b<a]]
Premise
Construct n
Applying the subset axiom...
35 EXIST(n):[Set(n) & ALL(a):[a n <=> a real & [0<a
& 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
36 Set(n) & ALL(a):[a n <=> a real & [0<a
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> a b]]]
E Spec, 35
37 Set(n)
Split, 36
38 ALL(a):[a n <=> a real & [0<a
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> a b]]]
Split, 36
Prove: x n => x real
Suppose...
39 x n
Premise
Apply definition of n.
40 x n <=> x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
U Spec, 38
41 [x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]]
& [x real & [0<x
& 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, 40
42 x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Split, 41
43 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]] => x n
Split, 41
44 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Detach, 42, 39
45 x real
Split, 44
As Required:
46 x n => x real
Conclusion, 39
n is a subset of the real numbers
47 ALL(a):[a n => a real]
U Gen, 46
Prove: 1 n
Apply the definition of n.
48 1 n <=> 1 real & [0<1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]]
U Spec, 38
49 [1 n => 1 real & [0<1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]]]
& [1 real & [0<1
& 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, 48
50 1 n => 1 real & [0<1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]]
Split, 49
Sufficient: For 1 n
51 1 real & [0<1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]] => 1 n
Split, 49
52 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
Premise
53 Set(sub)
Split, 52
54 ALL(c):[c sub => c real]
Split, 52
55 1 sub
Split, 52
56 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
=> 1 sub
Conclusion, 52
57 ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]
U Gen, 56
58 0<1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]
Join, 27, 57
59 1 real
& [0<1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> 1 b]]
Join, 14, 58
PA1
60 1 n
Detach, 51, 59
Prove: xn => x+1n
Suppose...
61 x n
Premise
Apply definition of n.
62 x n <=> x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
U Spec, 38
63 [x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]]
& [x real & [0<x
& 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, 62
64 x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Split, 63
65 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]] => x n
Split, 63
66 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Detach, 64, 61
67 x real
Split, 66
68 0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]
Split, 66
69 0<x
Split, 68
70 ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]
Split, 68
Apply definition of n.
71 x+1 n <=> x+1 real & [0<x+1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x+1 b]]
U Spec, 38
72 [x+1 n => x+1 real & [0<x+1
& 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 & [0<x+1
& 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, 71
73 x+1 n => x+1 real & [0<x+1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x+1 b]]
Split, 72
Sufficient: For x+1 n
Apply the defintion of n.
74 x+1 real & [0<x+1
& 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, 72
Prove: x+1 real
75 ALL(b):[x real & b real => x+b real]
U Spec, 3
76 x real & 1 real => x+1 real
U Spec, 75
77 x real & 1 real
Join, 67, 14
As Required:
78 x+1 real
Detach, 76, 77
Prove: x<x+1
Apply lemma.
79 ALL(b):[x real & b real & x+1=b => x<b]
U Spec, 33
80 x real & x+1 real & x+1=x+1 => x<x+1
U Spec, 79
81 x+1=x+1
Reflex
82 x real & x+1 real
Join, 67, 78
83 x real & x+1 real & x+1=x+1
Join, 82, 81
As Required:
84 x<x+1
Detach, 80, 83
Prove: 0<x+1
Apply transitivity of <.
85 ALL(b):ALL(c):[0 real & b real & c real & 0<b & b<c => 0<c]
U Spec, 29
86 ALL(c):[0 real & x real & c real & 0<x & x<c => 0<c]
U Spec, 85
87 0 real & x real & x+1 real & 0<x & x<x+1 => 0<x+1
U Spec, 86
88 0 real & x real
Join, 6, 67
89 0 real & x real & x+1 real
Join, 88, 78
90 0 real & x real & x+1 real & 0<x
Join, 89, 69
91 0 real & x real & x+1 real & 0<x & x<x+1
Join, 90, 84
As Required:
92 0<x+1
Detach, 87, 91
Prove: Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
=> x+1 sub
Suppose...
93 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
Premise
94 Set(sub)
Split, 93
95 ALL(c):[c sub => c real]
Split, 93
96 1 sub
Split, 93
97 ALL(c):[c sub => c+1 sub]
Split, 93
98 x sub => x+1 sub
U Spec, 97
Since xn...
99 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
=> x sub
U Spec, 70
100 x sub
Detach, 99, 93
101 x+1 sub
Detach, 98, 100
As Required:
102 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
=> x+1 sub
Conclusion, 93
As Required:
Generalizing...
103 ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x+1 b]
U Gen, 102
104 0<x+1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x+1 b]
Join, 92, 103
105 x+1 real
& [0<x+1
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x+1 b]]
Join, 78, 104
106 x+1 n
Detach, 74, 105
As Required:
107 x n => x+1 n
Conclusion, 61
PA2
108 ALL(a):[a n => a+1 n]
U Gen, 107
Prove: x n & y n & x+1=y+1 => x=y
Suppose...
109 x n & y n & x+1=y+1
Premise
110 x n
Split, 109
111 y n
Split, 109
112 x+1=y+1
Split, 109
Prove: x real
113 x n => x real
U Spec, 47
114 x real
Detach, 113, 110
Prove: y real
115 y n => y real
U Spec, 47
116 y real
Detach, 115, 111
Apply lemma for adding same to right cancellation.
117 ALL(b):ALL(c):[x real & b real & c real => [x=b <=> x+c=b+c]]
U Spec, 30
118 ALL(c):[x real & y real & c real => [x=y <=> x+c=y+c]]
U Spec, 117
119 x real & y real & 1 real => [x=y <=> x+1=y+1]
U Spec, 118
120 x real & y real
Join, 114, 116
121 x real & y real & 1 real
Join, 120, 14
122 x=y <=> x+1=y+1
Detach, 119, 121
123 [x=y => x+1=y+1] & [x+1=y+1 => x=y]
Iff-And, 122
124 x=y => x+1=y+1
Split, 123
125 x+1=y+1 => x=y
Split, 123
126 x=y
Detach, 125, 112
As Required:
127 x n & y n & x+1=y+1 => x=y
Conclusion, 109
Generalizing...
128 ALL(b):[x n & b n & x+1=b+1 => x=b]
U Gen, 127
PA3
129 ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
U Gen, 128
Prove: xn => ~x+1=1
Suppose...
130 x n
Premise
Apply definition of n.
131 x n <=> x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
U Spec, 38
132 [x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]]
& [x real & [0<x
& 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, 131
133 x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Split, 132
134 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]] => x n
Split, 132
135 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Detach, 133, 130
136 x real
Split, 135
137 0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]
Split, 135
Since xn...
138 0<x
Split, 137
139 ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]
Split, 137
Prove: ~x+1=1
Suppose to the contrary...
140 x+1=1
Premise
Prove: x=0
Add _1 to both sides.
141 ALL(b):ALL(c):[x+1 real & b real & c real => [x+1=b <=> x+1+c=b+c]]
U Spec, 30
142 ALL(c):[x+1 real & 1 real & c real => [x+1=1 <=> x+1+c=1+c]]
U Spec, 141
143 x+1 real & 1 real & _1 real => [x+1=1 <=> x+1+_1=1+_1]
U Spec, 142
Prove: x+1 real
144 ALL(b):[x real & b real => x+b real]
U Spec, 3
145 x real & 1 real => x+1 real
U Spec, 144
146 x real & 1 real
Join, 136, 14
As Required:
147 x+1 real
Detach, 145, 146
148 x+1 real & 1 real
Join, 147, 14
149 x+1 real & 1 real & _1 real
Join, 148, 31
150 x+1=1 <=> x+1+_1=1+_1
Detach, 143, 149
151 [x+1=1 => x+1+_1=1+_1] & [x+1+_1=1+_1 => x+1=1]
Iff-And, 150
152 x+1=1 => x+1+_1=1+_1
Split, 151
153 x+1+_1=1+_1 => x+1=1
Split, 151
154 x+1+_1=1+_1
Detach, 152, 140
Apply associative property of +.
155 ALL(b):ALL(c):[x real & b real & c real => x+b+c=x+(b+c)]
U Spec, 4
156 ALL(c):[x real & 1 real & c real => x+1+c=x+(1+c)]
U Spec, 155
157 x real & 1 real & _1 real => x+1+_1=x+(1+_1)
U Spec, 156
158 x real & 1 real
Join, 136, 14
159 x real & 1 real & _1 real
Join, 158, 31
160 x+1+_1=x+(1+_1)
Detach, 157, 159
161 x+(1+_1)=1+_1
Substitute, 160, 154
Apply definition of _ operator.
162 1 real => 1+_1=0
U Spec, 9
163 1+_1=0
Detach, 162, 14
164 x+0=0
Substitute, 163, 161
Apply definition of 0.
165 x real => x+0=x
U Spec, 7
166 x+0=x
Detach, 165, 136
As Required:
167 x=0
Substitute, 166, 164
168 0<0
Substitute, 167, 138
Apply definition of <.
169 ALL(b):[0 real & b real => [0<b <=> b+_0 pos]]
U Spec, 25
170 0 real & 0 real => [0<0 <=> 0+_0 pos]
U Spec, 169
171 0 real & 0 real
Join, 6, 6
172 [0 real & 0 real => [0<0 <=> 0+_0 pos]]
& [0 real & 0 real]
Join, 170, 171
173 0 real & 0 real => [0<0 <=> 0+_0 pos]
Split, 172
174 0 real & 0 real
Split, 172
175 0<0 <=> 0+_0 pos
Detach, 173, 174
176 [0<0 => 0+_0 pos] & [0+_0 pos => 0<0]
Iff-And, 175
177 0<0 => 0+_0 pos
Split, 176
178 0+_0 pos => 0<0
Split, 176
179 0+_0 pos
Detach, 177, 168
Apply definition of _ operator.
180 0 real => 0+_0=0
U Spec, 9
181 0+_0=0
Detach, 180, 6
182 0 pos
Substitute, 181, 179
Apply trichotomy rule.
183 0 real
=> [0=0 | 0 pos | _0 pos]
& ~[0=0 & 0 pos]
& ~[0=0 & _0 pos]
& ~[0 pos & _0 pos]
U Spec, 22
184 [0=0 | 0 pos | _0 pos]
& ~[0=0 & 0 pos]
& ~[0=0 & _0 pos]
& ~[0 pos & _0 pos]
Detach, 183, 6
185 0=0 | 0 pos | _0 pos
Split, 184
186 ~[0=0 & 0 pos]
Split, 184
187 ~[0=0 & _0 pos]
Split, 184
188 ~[0 pos & _0 pos]
Split, 184
189 0=0
Reflex
190 0=0 & 0 pos
Join, 189, 182
Obtain the contradiction...
191 0=0 & 0 pos & ~[0=0 & 0 pos]
Join, 190, 186
As Required:
By contradiction...
192 ~x+1=1
Conclusion, 140
193 x n => ~x+1=1
Conclusion, 130
PA4
194 ALL(a):[a n => ~a+1=1]
U Gen, 193
195 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
Premise
196 Set(sub)
Split, 195
197 ALL(c):[c sub => c real]
Split, 195
198 1 sub
Split, 195
199 ALL(c):[c sub => c+1 sub]
Split, 195
Prove: x n => x sub
Suppose...
200 x n
Premise
201 x n <=> x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
U Spec, 38
202 [x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]]
& [x real & [0<x
& 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, 201
203 x n => x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Split, 202
204 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]] => x n
Split, 202
205 x real & [0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]]
Detach, 203, 200
206 x real
Split, 205
207 0<x
& ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]
Split, 205
208 0<x
Split, 207
209 ALL(b):[Set(b)
& ALL(c):[c b => c real]
& 1 b
& ALL(c):[c b => c+1 b]
=> x b]
Split, 207
210 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
=> x sub
U Spec, 209
211 x sub
Detach, 210, 195
As Required:
212 x n => x sub
Conclusion, 200
213 ALL(a):[a n => a sub]
U Gen, 212
214 Set(sub)
& ALL(c):[c sub => c real]
& 1 sub
& ALL(c):[c sub => c+1 sub]
=> ALL(a):[a n => a sub]
Conclusion, 195
PA5
215 ALL(s):[Set(s)
& ALL(c):[c s => c real]
& 1 s
& ALL(c):[c s => c+1 s]
=> ALL(a):[a n => a s]]
U Gen, 214
216 Set(n) & ALL(a):[a n => a real]
Join, 37, 47
217 Set(n) & ALL(a):[a n => a real] & 1 n
Join, 216, 60
218 Set(n) & ALL(a):[a n => a real] & 1 n
& ALL(a):[a n => a+1 n]
Join, 217, 108
219 Set(n) & ALL(a):[a n => a real] & 1 n
& ALL(a):[a n => a+1 n]
& ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
Join, 218, 129
220 Set(n) & ALL(a):[a n => a real] & 1 n
& ALL(a):[a n => a+1 n]
& ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
& ALL(a):[a n => ~a+1=1]
Join, 219, 194
We have...
221 Set(n) & ALL(a):[a n => a real] & 1 n
& ALL(a):[a n => a+1 n]
& ALL(a):ALL(b):[a n & b n & a+1=b+1 => a=b]
& ALL(a):[a n => ~a+1=1]
& ALL(s):[Set(s)
& ALL(c):[c s => c real]
& 1 s
& ALL(c):[c s => c+1 s]
=> ALL(a):[a n => a s]]
Join, 220, 215
222 EXIST(nat):[Set(nat) & ALL(a):[a nat => a real] & 1 nat
& ALL(a):[a nat => a+1 nat]
& ALL(a):ALL(b):[a nat & b nat & a+1=b+1 => a=b]
& ALL(a):[a nat => ~a+1=1]
& ALL(s):[Set(s)
& ALL(c):[c s => c real]
& 1 s
& ALL(c):[c s => c+1 s]
=> ALL(a):[a nat => a s]]]
E Gen, 221
Prove: n is unique.
Suppose we have n' such that...
223 Set(n')
& ALL(a):[a n' => a real]
& 1 n'
& ALL(a):[a n' => a+1 n']
& ALL(a):ALL(b):[a n' & b n' & a+1=b+1 => a=b]
& ALL(a):[a n' => ~a+1=1]
& ALL(s):[Set(s)
& ALL(c):[c s => c real]
& 1 s
& ALL(c):[c s => c+1 s]
=> ALL(a):[a n' => a s]]
Premise
Splitting...
224 Set(n')
Split, 223
225 ALL(a):[a n' => a real]
Split, 223
226 1 n'
Split, 223
227 ALL(a):[a n' => a+1 n']
Split, 223
228 ALL(a):ALL(b):[a n' & b n' & a+1=b+1 => a=b]
Split, 223
229 ALL(a):[a n' => ~a+1=1]
Split, 223
230 ALL(s):[Set(s)
& ALL(c):[c s => c real]
& 1 s
& ALL(c):[c s => c+1 s]
=> ALL(a):[a n' => a s]]
Split, 223
Apply Set Equality axiom.
231 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c a <=> c b]]]
Set Equality
232 ALL(b):[Set(n) & Set(b) => [n=b <=> ALL(c):[c n <=> c b]]]
U Spec, 231
233 Set(n) & Set(n') => [n=n' <=> ALL(c):[c n <=> c n']]
U Spec, 232
234 Set(n) & Set(n')
Join, 37, 224
235 n=n' <=> ALL(c):[c n <=> c n']
Detach, 233, 234
236 [n=n' => ALL(c):[c n <=> c n']]
& [ALL(c):[c n <=> c n'] => n=n']
Iff-And, 235
237 n=n' => ALL(c):[c n <=> c n']
Split, 236
Sufficient: For n=n'
238 ALL(c):[c n <=> c n'] => n=n'
Split, 236
Sufficient: For ALL(a):[a n => a n']
Applying the principle of mathematical induction in n...
239 Set(n')
& ALL(c):[c n' => c real]
& 1 n'
& ALL(c):[c n' => c+1 n']
=> ALL(a):[a n => a n']
U Spec, 215
240 Set(n') & ALL(a):[a n' => a real]
Join, 224, 225
241 Set(n') & ALL(a):[a n' => a real] & 1 n'
Join, 240, 226
242 Set(n') & ALL(a):[a n' => a real] & 1 n'
& ALL(a):[a n' => a+1 n']
Join, 241, 227
243 ALL(a):[a n => a n']
Detach, 239, 242
244 Set(n)
& ALL(c):[c n => c real]
& 1 n
& ALL(c):[c n => c+1 n]
=> ALL(a):[a n' => a n]
U Spec, 230
245 Set(n) & ALL(a):[a n => a real]
Join, 37, 47
246 Set(n) & ALL(a):[a n => a real] & 1 n
Join, 245, 60
247 Set(n) & ALL(a):[a n => a real] & 1 n
& ALL(a):[a n => a+1 n]
Join, 246, 108
248 ALL(a):[a n' => a n]
Detach, 244, 247
249 x n => x n'
U Spec, 243
250 x n' => x n
U Spec, 248
251 [x n => x n'] & [x n' => x n]
Join, 249, 250
252 x n <=> x n'
Iff-And, 251
253 ALL(a):[a n <=> a n']
U Gen, 252
As Required:
254 n=n'
Detach, 238, 253