Below are a few simple informal and formal proofs I did in a math course. The problems (in blue) are from the course text. There's no claim that these proofs maximize elegance or economy, and I prefer to take more steps for more clarity.
Prove that the sum of an integer and its square is even.
The sum of an integer x and its square is x2 + x. Now, since x is either even or odd, there is some integer k such that either x = 2k if x is even or x = (2k + 1) if x is odd. If x = 2k, then x2 + x = (2k)2 + 2k, which equals 4k2 + 2k, which by factoring equals 2(2k2 + k), which is even. On the other hand, if x = (2k + 1), then x2 + x = (2k + 1)2 + (2k + 1), which equals 4k2 + 4k + 1 + 2k + 1, which equals 4k2 + 6k + 2, which by factoring equals 2(2k2 + 3k + 1), which is also even. Since x is arbitrary and the sum of x and its square is even whether x is even or odd, and since every integer is either even or odd, it follows that the sum of any integer and its square is even.
Prove that the sum of even integers is even.
So, assuming that Z = 'the set of integers' and ZE = 'set of even integers',
from 1 below derive : "x"y [ ( x Î ZE Ù y Î ZE ) ® ( ( x + y ) Î ZE ) ]
| 1. "x [ ( x Î ZE ) ® $k ( k Î Z Ù x = 2k ) ] | the definition of even | |
| 2. ( x Î ZE ) ® $k ( k Î Z Ù x = 2k ) | 1, universal instantiation (ui) | |
| 3. ( y Î ZE ) ® $k ( k Î Z Ù y = 2k ) | 1, ui | |
| 4. | x Î ZE Ù y Î ZE | assume |
| 5. | x Î ZE | 4, simplification (sim) |
| 6. | y Î ZE |
4, sim |
| 7. | $k ( k Î Z Ù x = 2k ) |
2, 5 modus ponens (mp) |
| 8. | $k ( k Î Z Ù y = 2k ) |
3, 6 mp |
| 9. | m Î Z Ù x = 2m | 7, existential instantiation (ei) |
| 10. | n Î Z Ù y = 2n | 8, ei |
| 11. | x = 2m | 9, sim |
| 12. | y = 2n | 10, sim |
| 13. | m Î Z | 9, sim |
| 14. | n Î Z | 10, sim |
| 15. | ( m + n ) Î Z | 13, 14 closure of Z under addition |
| 16. | ( x + y ) = ( 2m + 2n ) | 11, 12 addition |
| 17. | ( 2m + 2n ) = 2( m + n ) | 16, factoring |
| 18. | ( x + y ) = 2( m + n ) | 16, 17 transitivity of identity |
| 19. | 2( m + n ) Î ZE | 15, 18 definition of even |
| 20. | ( x + y ) Î ZE | 18, 19 identity |
| 21. ( x Î ZE Ù y Î ZE ) ® ( ( x + y ) Î ZE ) | 4 - 20 deduction theorem | |
| 22. "y [ ( x Î ZE Ù y Î ZE ) ® ( ( x + y ) Î ZE ) ] | 21, universal generalization (ug) | |
| 23. "x"y [ ( x Î ZE Ù y Î ZE ) ® ( ( x + y ) Î ZE ) ] | 22, ug | |
Prove that the number n is an even integer if and only if 3n + 2 = 6k + 2 for some integer k.
Prove: "n$k [ ( n Î Z Ù k Î Z ) ® [ ( n = 2k ) « ( 3n + 2 = 6k + 2 ) ] ]
| 1. | n Î Z Ù k Î Z | assume | |
| 2. | n = 2k | assume | |
| 3. | 2 = 6/3 | fact | |
| 4. | n = (6/3)k | 2, 3 identity | |
| 5. | 3n = 6k | 4, algebra | |
| 6. | 3n + 2 = 6k + 2 | 5, algebra | |
| 7. | ( n = 2k ) ® ( 3n + 2 = 6k + 2 ) | 2 - 6 deduction theorem | |
| 8. | 3n + 2 = 6k + 2 | assume | |
| 9. | 3n = 6k + 2 - 2 | 8, algebra | |
| 10. | 3n = 6k | 9, subtraction | |
| 11. | n = (6/3)k | 10, algebra | |
| 12. | 6/3 = 2 | fact | |
| 13. | n = 2k | 11, 12 identity | |
| 14. | ( 3n + 2 = 6k + 2 ) ® ( n = 2k ) | 8 - 13 deduction theorem | |
| 15. | [ ( n = 2k ) ® ( 3n + 2 = 6k + 2 ) ] Ù [ ( 3n + 2 = 6k + 2 ) ® ( n = 2k ) ] 7, 14 conjunction | ||
| 16. | ( n = 2k ) « ( 3n + 2 = 6k + 2 ) | 15, definition of « | |
| 17. ( n Î Z Ù k Î Z ) ® [ ( n = 2k ) « ( 3n + 2 = 6k + 2 ) ] | 1 - 16 deduction theorem | ||
| 18. $k [ ( n Î Z Ù k Î Z ) ® ( ( n = 2k ) « ( 3n + 2 = 6k + 2 ) ) ] | 17, existential generalization | ||
| 19. "n$k [ ( n Î Z Ù k Î Z ) ® ( ( n = 2k ) « ( 3n + 2 = 6k + 2 ) ) ] | 18, universal generalization | ||
Same informally: If n and k are integers, then if n is even, n = 2k and n = (6/3)k since 6/3 = 2. Now by algebra, if n = (6/3)k, then 3n = 6k, and moreover 3n + 2 = 6k + 2, which is half of what was to be shown. For the other half, if 3n + 2 = 6k + 2, then by algebra 3n = 6k + 2 - 2, which equals 3n = 6k, in which case n = (6/3)k, and so n = 2k; which covers all that was to be shown.
Prove by induction that n2 > ( 5n + 10 ) for all n > 6.
Base:
72 > 5(7) + 10
49 > 35 + 10
49 > 45
Thus: $n ( n > 6 Ù n2 > 5n + 10 )
Hypothesis: "n [ ( n > 6 ) ® ( n2 > 5n + 10 ) ]
Inductive hypo: "k [ ( k > 6 ) ® ( k2 > 5k + 10 ) ] ® "k [ ( k > 6 ) ® ( (k + 1)2 > 5(k + 1) + 10 ) ]
So from 1 below we must derive : "k [ ( k > 6 ) ® ( (k + 1)2 > 5(k + 1) + 10 ) ]
1. "k [ ( k > 6 ) ® ( k2 > 5k + 10 ) ] |
assume | |
| 2. | k > 6 | assume |
| 3. | ( k > 6 ) ® ( k2 > 5k + 10 ) | 1, universal instantiation |
| 4. | k2 > 5k + 10 | 2, 3 modus ponens |
| 5. | (k + 1)2 = k2 + 2k + 1 | fact |
| 6. | (k + 1)2 > (5k + 10) + 2k + 1 | 5 made unequal by substituting k2 as per 4 |
| 7. | (k + 1)2 > 5k + 10 + 2(2) + 1 | 2 and since 6 > 2, a fortiori k > 2 [*] |
| 8. | (k + 1)2 > 5k + 10 + 4 + 1 | 7, multiplication |
| 9. | (k + 1)2 > 5k + 10 + 5 | 8, addition |
| 10. | (k + 1)2 > 5k + 5 + 10 | 9, commutativity |
| 11. | (k + 1)2 > 5(k + 1) + 10 | 10, factoring |
| 12. ( k > 6 ) ® ( (k + 1)2 > 5(k + 1) + 10 ) | 2 - 11 deduction theorem | |
| 13. "k [ ( k > 6 ) ® ( (k + 1)2 > 5(k + 1) + 10 ) ] | 12, universal generalization | |
[*] Note that the change of a k in step 6 to '2' in step 7 expresses the transitivity of the greater than relation (ie, '>' ):
| 1. "x"y"z [ (( x > y ) Ù ( y > z )) ® ( x > z ) ] | by definition of transitive |
| 2. "y"z [ (( k > y ) Ù ( y > z )) ® ( k > z ) ] | 1, universal instantiation (ui) |
| 3. "z [ (( k > 6 ) Ù ( 6 > z )) ® ( k > z ) ] | 2, ui |
| 4. (( k > 6 ) Ù ( 6 > 2 )) ® ( k > 2 ) | 3, ui |
In words: if we know that a > b (and by step 2 we know that k > 6) and we also know b > c (as we know 6 > 2), then we know that a > c (and so we know that k > 2, and thus expressing a greater than relation, step 7 must be true).
I consider these proofs to be logical members of my art portfolio where art is defined as sensible articulation of physical or abstract data structures. Such a common definition also seems warranted by the subjective experience that creating or appreciating a piece of art and creating or appreciating a proof both induce similar aesthetic experiences. This may in turn be a consequence of common cognitive structures underlying interpretation and expression of representational data structures.
(© 2006 Ian Goddard)