Past exam of the mathematics course of the University of Cambridge / 2024 / iii / Paper 120 / 3 / a / Solution

Under the Implicational Curry-Howard correspondence, propositions are simple types and assumptions are typed variables. The natural-deduction rulescorrespond respectively to the typing rulesAn assumption $x:A$ corresponds to the variable rule. Induction on a proof converts each rule into the matching typing construction; induction on a typing derivation reverses the process. Thus derivability of an implicational formula from assumptions is equivalent to inhabitation of its corresponding type.