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.