THEOREM

*******

Addition on the natural numbers is commutative.

ALL(a):ALL(b):[a e n & b e n => a+b=b+a]

PROOF

*****

Peano's Axioms

1 Set(n)

Axiom

2 0 e n

Axiom

3 ALL(a):[a e n => s(a) e n]

Axiom

4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]

Axiom

5 ALL(a):[a e n => ~s(a)=0]

Axiom

6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]

=> [0 e a & ALL(b):[b e a => s(b) e a]

=> ALL(b):[b e n => b e a]]]

Axiom

Define +

7 ALL(a):ALL(b):[a e n & b e n => a+b e n]

Axiom

8 ALL(a):[a e n => a+0=a]

Axiom

9 ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a+b)]

Axiom

Suppose...

10 x e n

Premise

11 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & x+s(b)=s(x)+b]]

Subset, 1

12 Set(p) & ALL(b):[b e p <=> b e n & x+s(b)=s(x)+b]

E Spec, 11

Define: p

13 Set(p)

Split, 12

14 ALL(b):[b e p <=> b e n & x+s(b)=s(x)+b]

Split, 12

15 Set(p) & ALL(b):[b e p => b e n]

=> [0 e p & ALL(b):[b e p => s(b) e p]

=> ALL(b):[b e n => b e p]]

U Spec, 6

16 y e p

Premise

17 y e p <=> y e n & x+s(y)=s(x)+y

U Spec, 14

18 [y e p => y e n & x+s(y)=s(x)+y]

& [y e n & x+s(y)=s(x)+y => y e p]

Iff-And, 17

19 y e p => y e n & x+s(y)=s(x)+y

Split, 18

20 y e n & x+s(y)=s(x)+y => y e p

Split, 18

21 y e n & x+s(y)=s(x)+y

Detach, 19, 16

22 y e n

Split, 21

23 ALL(b):[b e p => b e n]

4 Conclusion, 16

24 Set(p) & ALL(b):[b e p => b e n]

Join, 13, 23

Sufficient: For ALL(b):[b e n => b e p]

25 0 e p & ALL(b):[b e p => s(b) e p]

=> ALL(b):[b e n => b e p]

Detach, 15, 24

26 0 e p <=> 0 e n & x+s(0)=s(x)+0

U Spec, 14

27 [0 e p => 0 e n & x+s(0)=s(x)+0]

& [0 e n & x+s(0)=s(x)+0 => 0 e p]

Iff-And, 26

28 0 e p => 0 e n & x+s(0)=s(x)+0

Split, 27

Sufficient:

29 0 e n & x+s(0)=s(x)+0 => 0 e p

Split, 27

30 ALL(b):[x e n & b e n => x+s(b)=s(x+b)]

U Spec, 9

31 x e n & 0 e n => x+s(0)=s(x+0)

U Spec, 30

32 x e n & 0 e n

Join, 10, 2

33 x+s(0)=s(x+0)

Detach, 31, 32

34 x e n => x+0=x

U Spec, 8

35 x+0=x

Detach, 34, 10

36 x+s(0)=s(x)

Substitute, 35, 33

37 x e n => s(x) e n

U Spec, 3

38 s(x) e n

Detach, 37, 10

39 s(x) e n => s(x)+0=s(x)

U Spec, 8, 38

40 s(x)+0=s(x)

Detach, 39, 38

41 x+s(0)=s(x)+0

Substitute, 40, 36

42 0 e n & x+s(0)=s(x)+0

Join, 2, 41

As Required:

43 0 e p

Detach, 29, 42

Suppose...

44 y e p

Premise

45 y e p <=> y e n & x+s(y)=s(x)+y

U Spec, 14

46 [y e p => y e n & x+s(y)=s(x)+y]

& [y e n & x+s(y)=s(x)+y => y e p]

Iff-And, 45

47 y e p => y e n & x+s(y)=s(x)+y

Split, 46

48 y e n & x+s(y)=s(x)+y => y e p

Split, 46

49 y e n & x+s(y)=s(x)+y

Detach, 47, 44

50 y e n

Split, 49

51 x+s(y)=s(x)+y

Split, 49

52 y e n => s(y) e n

U Spec, 3

53 s(y) e n

Detach, 52, 50

54 s(y) e p <=> s(y) e n & x+s(s(y))=s(x)+s(y)

U Spec, 14, 53

55 [s(y) e p => s(y) e n & x+s(s(y))=s(x)+s(y)]

& [s(y) e n & x+s(s(y))=s(x)+s(y) => s(y) e p]

Iff-And, 54

56 s(y) e p => s(y) e n & x+s(s(y))=s(x)+s(y)

Split, 55

Sufficient: For s(y) e p

57 s(y) e n & x+s(s(y))=s(x)+s(y) => s(y) e p

Split, 55

58 ALL(b):[x e n & b e n => x+s(b)=s(x+b)]

U Spec, 9

59 x e n & s(y) e n => x+s(s(y))=s(x+s(y))

U Spec, 58, 53

60 x e n & s(y) e n

Join, 10, 53

61 x+s(s(y))=s(x+s(y))

Detach, 59, 60

62 ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a+b)]

Copy, 9

63 x+s(s(y))=s(s(x)+y)

Substitute, 51, 61

64 ALL(b):[s(x) e n & b e n => s(x)+s(b)=s(s(x)+b)]

U Spec, 62, 38

65 s(x) e n & y e n => s(x)+s(y)=s(s(x)+y)

U Spec, 64

66 s(x) e n & y e n

Join, 38, 50

67 s(x)+s(y)=s(s(x)+y)

Detach, 65, 66

68 x+s(s(y))=s(x)+s(y)

Substitute, 67, 63

69 s(y) e n & x+s(s(y))=s(x)+s(y)

Join, 53, 68

70 s(y) e p

Detach, 57, 69

71 ALL(b):[b e p => s(b) e p]

4 Conclusion, 44

72 0 e p & ALL(b):[b e p => s(b) e p]

Join, 43, 71

As Required:

73 ALL(b):[b e n => b e p]

Detach, 25, 72

74 y e n

Premise

75 y e n => y e p

U Spec, 73

76 y e p

Detach, 75, 74

77 y e p <=> y e n & x+s(y)=s(x)+y

U Spec, 14

78 [y e p => y e n & x+s(y)=s(x)+y]

& [y e n & x+s(y)=s(x)+y => y e p]

Iff-And, 77

79 y e p => y e n & x+s(y)=s(x)+y

Split, 78

80 y e n & x+s(y)=s(x)+y => y e p

Split, 78

81 y e n & x+s(y)=s(x)+y

Detach, 79, 76

82 y e n

Split, 81

83 x+s(y)=s(x)+y

Split, 81

84 ALL(b):[b e n => x+s(b)=s(x)+b]

4 Conclusion, 74

As Required:

85 ALL(a):[a e n => ALL(b):[b e n => a+s(b)=s(a)+b]]

4 Conclusion, 10

86 x e n & y e n

Premise

87 x e n

Split, 86

88 y e n

Split, 86

89 x e n => ALL(b):[b e n => x+s(b)=s(x)+b]

U Spec, 85

90 ALL(b):[b e n => x+s(b)=s(x)+b]

Detach, 89, 87

91 y e n => x+s(y)=s(x)+y

U Spec, 90

92 x+s(y)=s(x)+y

Detach, 91, 88

LEMMA

*****

As Required:

93 ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a)+b]

4 Conclusion, 86

Suppose...

94 x e n

Premise

95 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & x+b=b+x]]

Subset, 1

96 Set(p') & ALL(b):[b e p' <=> b e n & x+b=b+x]

E Spec, 95

Define: p'

97 Set(p')

Split, 96

98 ALL(b):[b e p' <=> b e n & x+b=b+x]

Split, 96

99 Set(p') & ALL(b):[b e p' => b e n]

=> [0 e p' & ALL(b):[b e p' => s(b) e p']

=> ALL(b):[b e n => b e p']]

U Spec, 6

Suppose...

100 y e p'

Premise

101 y e p' <=> y e n & x+y=y+x

U Spec, 98

102 [y e p' => y e n & x+y=y+x]

& [y e n & x+y=y+x => y e p']

Iff-And, 101

103 y e p' => y e n & x+y=y+x

Split, 102

104 y e n & x+y=y+x => y e p'

Split, 102

105 y e n & x+y=y+x

Detach, 103, 100

106 y e n

Split, 105

107 ALL(b):[b e p' => b e n]

4 Conclusion, 100

108 Set(p') & ALL(b):[b e p' => b e n]

Join, 97, 107

Sufficient: For ALL(b):[b e n => b e p']

109 0 e p' & ALL(b):[b e p' => s(b) e p']

=> ALL(b):[b e n => b e p']

Detach, 99, 108

110 0 e p' <=> 0 e n & x+0=0+x

U Spec, 98

111 [0 e p' => 0 e n & x+0=0+x]

& [0 e n & x+0=0+x => 0 e p']

Iff-And, 110

112 0 e p' => 0 e n & x+0=0+x

Split, 111

113 ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a)+b]

Copy, 93

114 0 e n & x+0=0+x => 0 e p'

Split, 111

115 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & a+0=0+a]]

Subset, 1

116 Set(p2) & ALL(a):[a e p2 <=> a e n & a+0=0+a]

E Spec, 115

Prove: ALL(a):[a e n => a+0=0+a]

Define: p2

117 Set(p2)

Split, 116

118 ALL(a):[a e p2 <=> a e n & a+0=0+a]

Split, 116

119 Set(p2) & ALL(b):[b e p2 => b e n]

=> [0 e p2 & ALL(b):[b e p2 => s(b) e p2]

=> ALL(b):[b e n => b e p2]]

U Spec, 6

120 y e p2

Premise

121 y e p2 <=> y e n & y+0=0+y

U Spec, 118

122 [y e p2 => y e n & y+0=0+y]

& [y e n & y+0=0+y => y e p2]

Iff-And, 121

123 y e p2 => y e n & y+0=0+y

Split, 122

124 y e n & y+0=0+y => y e p2

Split, 122

125 y e n & y+0=0+y

Detach, 123, 120

126 y e n

Split, 125

127 ALL(b):[b e p2 => b e n]

4 Conclusion, 120

128 Set(p2) & ALL(b):[b e p2 => b e n]

Join, 117, 127

Sufficient: For ALL(b):[b e n => b e p2]

129 0 e p2 & ALL(b):[b e p2 => s(b) e p2]

=> ALL(b):[b e n => b e p2]

Detach, 119, 128

130 0 e p2 <=> 0 e n & 0+0=0+0

U Spec, 118

131 [0 e p2 => 0 e n & 0+0=0+0]

& [0 e n & 0+0=0+0 => 0 e p2]

Iff-And, 130

132 0 e p2 => 0 e n & 0+0=0+0

Split, 131

133 0 e n & 0+0=0+0 => 0 e p2

Split, 131

134 ALL(b):[0 e n & b e n => 0+b e n]

U Spec, 7

135 0 e n & 0 e n => 0+0 e n

U Spec, 134

136 0 e n & 0 e n

Join, 2, 2

137 0+0 e n

Detach, 135, 136

138 0+0=0+0

Reflex, 137

139 0 e n & 0+0=0+0

Join, 2, 138

As Required:

140 0 e p2

Detach, 133, 139

Suppose...

141 y e p2

Premise

142 y e p2 <=> y e n & y+0=0+y

U Spec, 118

143 [y e p2 => y e n & y+0=0+y]

& [y e n & y+0=0+y => y e p2]

Iff-And, 142

144 y e p2 => y e n & y+0=0+y

Split, 143

145 y e n & y+0=0+y => y e p2

Split, 143

146 y e n & y+0=0+y

Detach, 144, 141

147 y e n

Split, 146

148 y+0=0+y

Split, 146

149 y e n => s(y) e n

U Spec, 3

150 s(y) e n

Detach, 149, 147

151 s(y) e p2 <=> s(y) e n & s(y)+0=0+s(y)

U Spec, 118, 150

152 [s(y) e p2 => s(y) e n & s(y)+0=0+s(y)]

& [s(y) e n & s(y)+0=0+s(y) => s(y) e p2]

Iff-And, 151

153 s(y) e p2 => s(y) e n & s(y)+0=0+s(y)

Split, 152

Sufficient: For s(y) e p2

154 s(y) e n & s(y)+0=0+s(y) => s(y) e p2

Split, 152

155 ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a)+b]

Copy, 93

156 ALL(b):[y e n & b e n => y+s(b)=s(y)+b]

U Spec, 155

157 y e n & 0 e n => y+s(0)=s(y)+0

U Spec, 156

158 y e n & 0 e n

Join, 147, 2

159 y+s(0)=s(y)+0

Detach, 157, 158

160 ALL(b):[y e n & b e n => y+s(b)=s(y+b)]

U Spec, 9

161 y e n & 0 e n => y+s(0)=s(y+0)

U Spec, 160

162 y e n & 0 e n

Join, 147, 2

163 y+s(0)=s(y+0)

Detach, 161, 162

164 ALL(b):[y e n & b e n => y+b e n]

U Spec, 7

165 y e n & 0 e n => y+0 e n

U Spec, 164

166 y+0 e n

Detach, 165, 158

167 y+0 e n => s(y+0) e n

U Spec, 3, 166

168 s(y+0) e n

Detach, 167, 166

169 s(y+0)=s(y+0)

Reflex, 168

170 s(y+0)=s(0+y)

Substitute, 148, 169

171 ALL(b):[0 e n & b e n => 0+s(b)=s(0+b)]

U Spec, 9

172 0 e n & y e n => 0+s(y)=s(0+y)

U Spec, 171

173 0 e n & y e n

Join, 2, 147

174 0+s(y)=s(0+y)

Detach, 172, 173

175 s(y)+0=y+s(0)

Sym, 159

176 s(y)+0=s(y+0)

Substitute, 163, 175

177 s(y)+0=s(0+y)

Substitute, 170, 176

178 s(y)+0=0+s(y)

Substitute, 174, 177

179 s(y) e n & s(y)+0=0+s(y)

Join, 150, 178

180 s(y) e p2

Detach, 154, 179

181 ALL(b):[b e p2 => s(b) e p2]

4 Conclusion, 141

182 0 e p2 & ALL(b):[b e p2 => s(b) e p2]

Join, 140, 181

183 ALL(b):[b e n => b e p2]

Detach, 129, 182

184 y e n

Premise

185 y e n => y e p2

U Spec, 183

186 y e p2

Detach, 185, 184

187 y e p2 <=> y e n & y+0=0+y

U Spec, 118

188 [y e p2 => y e n & y+0=0+y]

& [y e n & y+0=0+y => y e p2]

Iff-And, 187

189 y e p2 => y e n & y+0=0+y

Split, 188

190 y e n & y+0=0+y => y e p2

Split, 188

191 y e n & y+0=0+y

Detach, 189, 186

192 y e n

Split, 191

193 y+0=0+y

Split, 191

194 ALL(a):[a e n => a+0=0+a]

4 Conclusion, 184

195 x e n => x+0=0+x

U Spec, 194

196 x+0=0+x

Detach, 195, 94

197 0 e n & x+0=0+x

Join, 2, 196

As Required:

198 0 e p'

Detach, 114, 197

Suppose...

199 y e p'

Premise

200 y e p' <=> y e n & x+y=y+x

U Spec, 98

201 [y e p' => y e n & x+y=y+x]

& [y e n & x+y=y+x => y e p']

Iff-And, 200

202 y e p' => y e n & x+y=y+x

Split, 201

203 y e n & x+y=y+x => y e p'

Split, 201

204 y e n & x+y=y+x

Detach, 202, 199

205 y e n

Split, 204

206 x+y=y+x

Split, 204

207 y e n => s(y) e n

U Spec, 3

208 s(y) e n

Detach, 207, 205

209 s(y) e p' <=> s(y) e n & x+s(y)=s(y)+x

U Spec, 98, 208

210 [s(y) e p' => s(y) e n & x+s(y)=s(y)+x]

& [s(y) e n & x+s(y)=s(y)+x => s(y) e p']

Iff-And, 209

211 s(y) e p' => s(y) e n & x+s(y)=s(y)+x

Split, 210

Sufficient: For s(y) e p'

212 s(y) e n & x+s(y)=s(y)+x => s(y) e p'

Split, 210

213 ALL(b):[x e n & b e n => x+s(b)=s(x+b)]

U Spec, 9

214 x e n & y e n => x+s(y)=s(x+y)

U Spec, 213

215 x e n & y e n

Join, 94, 205

216 x+s(y)=s(x+y)

Detach, 214, 215

217 x+s(y)=s(y+x)

Substitute, 206, 216

218 ALL(b):[y e n & b e n => y+s(b)=s(y+b)]

U Spec, 9

219 y e n & x e n => y+s(x)=s(y+x)

U Spec, 218

220 y e n & x e n

Join, 205, 94

221 y+s(x)=s(y+x)

Detach, 219, 220

222 ALL(a):ALL(b):[a e n & b e n => a+s(b)=s(a)+b]

Copy, 93

223 ALL(b):[y e n & b e n => y+s(b)=s(y)+b]

U Spec, 222

224 y e n & x e n => y+s(x)=s(y)+x

U Spec, 223

225 y+s(x)=s(y)+x

Detach, 224, 220

226 x+s(y)=y+s(x)

Substitute, 221, 217

227 x+s(y)=s(y)+x

Substitute, 225, 226

228 s(y) e n & x+s(y)=s(y)+x

Join, 208, 227

229 s(y) e p'

Detach, 212, 228

230 ALL(b):[b e p' => s(b) e p']

4 Conclusion, 199

231 0 e p' & ALL(b):[b e p' => s(b) e p']

Join, 198, 230

As Required:

232 ALL(b):[b e n => b e p']

Detach, 109, 231

233 y e n

Premise

234 y e n => y e p'

U Spec, 232

235 y e p'

Detach, 234, 233

236 y e p' <=> y e n & x+y=y+x

U Spec, 98

237 [y e p' => y e n & x+y=y+x]

& [y e n & x+y=y+x => y e p']

Iff-And, 236

238 y e p' => y e n & x+y=y+x

Split, 237

239 y e n & x+y=y+x => y e p'

Split, 237

240 y e n & x+y=y+x

Detach, 238, 235

241 y e n

Split, 240

242 x+y=y+x

Split, 240

243 ALL(b):[b e n => x+b=b+x]

4 Conclusion, 233

244 ALL(a):[a e n => ALL(b):[b e n => a+b=b+a]]

4 Conclusion, 94

245 x e n & y e n

Premise

246 x e n

Split, 245

247 y e n

Split, 245

248 x e n => ALL(b):[b e n => x+b=b+x]

U Spec, 244

249 ALL(b):[b e n => x+b=b+x]

Detach, 248, 246

250 y e n => x+y=y+x

U Spec, 249

251 x+y=y+x

Detach, 250, 247

As Required:

252 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]

4 Conclusion, 245