Next | Types Are Theorems; Programs Are Proofs | 12 |
Write a proof
To prove a → b, assume a and present an argument for b (→I)
If a is proved, and if a → b is proved, then b is proved (→E)
For example, let's prove (a → b) → (b → c) → (a → c)
1 | Assume a → b | ||||||||||||||||
2 | Assume b → c | ||||||||||||||||
3 | Assume a | ||||||||||||||||
4 | From (3) and (1), conclude b
|
Could we stop at step 7 and conclude (b → c) → (a → c)?
No, because assumption 1 is still undischarged
Next | Next |