Next | Types Are Theorems; Programs Are Proofs | 13 |

1 | Assume a
| ||

2 | Assume b
| ||

3 | From (2) and (1), conclude b → a
| (→I) | (discharges 2) |

4 | From (1) and (3), conclude a → (b → a)
| (→I) | (discharges 1) |

What if we did this instead:

1 | Assume a
| ||

2 | Assume b
| ||

3 | From (2) and (1), conclude b → a
| (→I) | (discharges 2) |

4 | From (2) and (3), conclude b → (b → a)
| (→I) | (discharges 2) |

`No`, because assumption 1 is still undischargedSo the proof is incomplete

(Discharging assumption 2 twice is actually OK)

What if we did this instead:

1 | Assume a
| ||

2 | Assume b
| ||

3 | From (2) and (1), conclude b → a
| (→I) | (discharges 2) |

4 | From (2) and (3), conclude b → (b → a)
| (→I) | (discharges 2) |

5 | From (1) and (4), conclude a → (b → (b → a))
| (→I) | (discharges 1) |

Yeah, that's okay.

By the way,

`a -> (b -> (b -> a))`is inhabited:

foo a = \b -> (\b -> a) :: a -> (b -> (b -> a))

Next | Next |