next up previous
Next: April 3, 2000 Up: Lecture Notes Previous: Tuesday, March 21, 2000

Solution to (part of) Homework 8:

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.



Randall Holmes
2000-05-05