Next Types Are Theorems; Programs Are Proofs 12

How to decide if a proposition is true

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

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

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

7From (2) and (6), conclude (bc) → (ac)
(→I) (discharges 2)

8From (1) and (7), conclude (ab) → (bc) → (ac)
(→I) (discharges 1)


Next Next