Next Types Are Theorems; Programs Are Proofs 12

How to decide if a proposition is true

1Assume a → b
2Assume b → c
3Assume a
4From (3) and (1), conclude b
(→E)

5From (4) and (2), conclude c
(→E)

6From (3) and (5), conclude a → c
(→I) (discharges 3)

7From (2) and (6), conclude (b → c) → (a → c)
(→I) (discharges 2)

8From (1) and (7), conclude (a → b) → (b → c) → (a → c)
(→I) (discharges 1)


Next Next