Goal: (Ax.Even(x) | Odd(x))
Prove by induction on x.
Goal (basis step): Even(0) | Odd(0)
Intuitively, this is true because 0 is even!
Goal: Even(0)
Goal (expand definition): (Ey.y+y=0)
The obvious choice for y is 0 itself.
1. 0+0=0 ax. 3, univ. elim.
2. (Ey.y+y=0) exist. intro.
3. Even(0) definition of Even, line 2
4. Even(0) | Odd(0) disj. intro (special) line 3
Now we set up the box for the induction step:
| 5. Even(a) | Odd(a) inductive hypothesis
| Goal: Even(a') | Odd(a')
The disjunctive form of the inductive hypothesis suggests a proof
by cases.
| | 6. Even(a) subpremise for proof by cases using line 5 (case 1)
| | 7. (Ey.y+y=a) definition of Even, line 6
Intuitively, if a is even, we expect a' to be odd, and a proof
of Odd(a') will certainly allow us to prove Even(a') | Odd(a')
| | Goal: Odd(a') = (Ez.z+z'=a')
| | | 8. Heart + Heart = a witness intro line 7
| | | 9. (Heart + Heart)' = a' substitution property of equality (or ax. 2)
line 8
| | | 10. Heart + Heart' = a' ax. 4, univ. elim.
| | | 11. (Ez.z+z'=a') exist. intro. line 10
| | 12. (Ez.z+z'=a') exist. elim. lines 8-11
| | 13. Odd(a') definition of Odd
| | 14. Even(a') | Odd(a') disj. intro(special), line 13
| 15. Even(a) -> (Even(a') | Odd(a')) imp. intro. lines 6-14
| | 16. Odd(a) subpremise for proof by cases using line 5 (case 2)
| | 17. (Ey.y+y'=a) definition of Odd, line 16
Intuitively, if a is odd, we expect a' to be even, and a proof
of Even(a') will certainly allow us to prove Even(a') | Odd(a')
| | Goal: Even(a') = (Ez.z+z=a')
| | | 18. Club + Club' = a witness intro line 17
| | | 19. (Club + Club')' = a' substitution property of equality (or ax. 2),
line 18
| | | 20. (Club' + Club)' = a' commutativity of addition, prop =, line 19
| | | 21. (Club' + Club') = a' ax. 4, univ. elim, line 20
| | | 22. (Ez.z+z=a') exist. intro. line 21 (the witness is Club')
| | 23. (Ez.z+z=a') exist. elim. lines 18-22
| | 24. Even(a') line 23, definition of Even
| | 25. Even(a') | Odd(a') disj. intro(special), line 24
| 26. Odd(a) -> (Even(a') | Odd(a')) imp. intro. lines 16-25
| 27. Even(a') | Odd(a') proof by cases, lines 5, 15, 26
(or one could omit lines 15, 26 and say
proof by cases, lines 5, 6-14, 16-25)
28. (Ax.(Even(x) | Odd(x))) math induction, lines 4, 5-27.
Different forms of the definition of Odd will give somewhat different proofs.