| 311 | 311 |
Step_3 = eq(o(e, e), e) by Identity with Step_2, Step_1
|
| 312 | 312 |
qed
|
| 313 | 313 |
===> ok
|
|
314 |
|
|
315 |
Number Theory
|
|
316 |
-------------
|
|
317 |
|
|
318 |
If y is odd, then y+1 is even.
|
|
319 |
|
|
320 |
The variable names used here are kind of painful, in order to avoid name clashes.
|
|
321 |
Perhaps the new variable introduced in UG and EG doesn't have to be unique?
|
|
322 |
As long as it's not the same as any atom already in P. (This sounds familiar.)
|
|
323 |
|
|
324 |
given
|
|
325 |
UG = P ; X{term} ; V{unique atom} |- forall(V, P)[X -> V]
|
|
326 |
UI = forall(X, P) ; V{term} |- P[X -> V]
|
|
327 |
EG = P ; X{term} ; V{unique atom} |- exists(V, P)[X -> V]
|
|
328 |
block EI
|
|
329 |
case
|
|
330 |
Let = exists(X, P) ; V{unique local atom} |- P[X -> V]
|
|
331 |
Then = P |- P
|
|
332 |
end
|
|
333 |
end
|
|
334 |
|
|
335 |
Weakening = biimpl(X, Y) |- impl(X, Y)
|
|
336 |
Reverse_Weakening = biimpl(X, Y) |- impl(Y, X)
|
|
337 |
Modus_Ponens = P ; impl(P, Q) |- Q
|
|
338 |
|
|
339 |
block Suppose
|
|
340 |
case
|
|
341 |
Supposition = A{term} |- A
|
|
342 |
Conclusion = P ; Q |- impl(P, Q)
|
|
343 |
end
|
|
344 |
end
|
|
345 |
|
|
346 |
Defn_of_Even = |- forall(n, biimpl(even(n), exists(m, eq(n, add(m, m)))))
|
|
347 |
Defn_of_Odd = |- forall(n, biimpl(odd(n), exists(k, eq(n, add(add(k, k), c(1))))))
|
|
348 |
|
|
349 |
Add_One_to_Both_Sides = eq(X, Y) |- eq(add(X, c(1)), add(Y, c(1)))
|
|
350 |
Provisional_Algebra = eq(X, add(add(add(A, B), C), D)) |- eq(X, add(add(A, C), add(B, D)))
|
|
351 |
|
|
352 |
show
|
|
353 |
forall(y, impl(odd(y), even(add(y, c(1)))))
|
|
354 |
proof
|
|
355 |
block Suppose
|
|
356 |
case
|
|
357 |
Step_1 = odd(x) by Supposition with odd(x)
|
|
358 |
Step_2 = forall(n, biimpl(odd(n), exists(k, eq(n, add(add(k, k), c(1)))))) by Defn_of_Odd
|
|
359 |
Step_3 = biimpl(odd(x), exists(k, eq(x, add(add(k, k), c(1))))) by UI with Step_2, x
|
|
360 |
Step_4 = impl(odd(x), exists(k, eq(x, add(add(k, k), c(1))))) by Weakening with Step_3
|
|
361 |
Step_5 = exists(k, eq(x, add(add(k, k), c(1)))) by Modus_Ponens with Step_1, Step_4
|
|
362 |
block EI
|
|
363 |
case
|
|
364 |
Step_6 = eq(x, add(add(j, j), c(1))) by Let with Step_5, j
|
|
365 |
Step_7 = eq(add(x, c(1)), add(add(add(j, j), c(1)), c(1))) by Add_One_to_Both_Sides with Step_6
|
|
366 |
Step_8 = eq(add(x, c(1)), add(add(j, c(1)), add(j, c(1)))) by Provisional_Algebra with Step_7
|
|
367 |
Step_9 = exists(m, eq(add(x, c(1)), add(m, m))) by EG with Step_8, add(j, c(1)), m
|
|
368 |
|
|
369 |
Step_10 = forall(n, biimpl(even(n), exists(m, eq(n, add(m, m))))) by Defn_of_Even
|
|
370 |
Step_11 = biimpl(even(add(x, c(1))), exists(m, eq(add(x, c(1)), add(m, m)))) by UI with Step_10, add(x, c(1))
|
|
371 |
Step_12 = impl(exists(m, eq(add(x, c(1)), add(m, m))), even(add(x, c(1)))) by Reverse_Weakening with Step_11
|
|
372 |
Step_13 = even(add(x, c(1))) by Modus_Ponens with Step_9, Step_12
|
|
373 |
Step_14 = even(add(x, c(1))) by Then with Step_13
|
|
374 |
end
|
|
375 |
end
|
|
376 |
Step_15 = impl(odd(x), even(add(x, c(1)))) by Conclusion with Step_1, Step_14
|
|
377 |
end
|
|
378 |
end
|
|
379 |
Step_16 = forall(y, impl(odd(y), even(add(y, c(1))))) by UG with Step_15, x, y
|
|
380 |
qed
|
|
381 |
===> ok
|