Under the <Implicational Curry-Howard correspondence>, propositions are simple types and assumptions are typed variables. The natural-deduction rules
$$
\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}
\qquad\text{and}\qquad
\frac{\Gamma\vdash A\to B\quad\Gamma\vdash A}{\Gamma\vdash B}
$$
correspond respectively to the typing rules
$$
\frac{\Gamma,x:A\vdash M:B}{\Gamma\vdash\lambda x.M:A\to B},
\qquad
\frac{\Gamma\vdash M:A\to B\quad\Gamma\vdash N:A}{\Gamma\vdash MN:B}.
$$
An 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.

Solution

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

{c}

In the implicational fragments, assumptions correspond to typed variables, implication introduction to lambda abstraction, and implication elimination to function application. Typing derivations in the simply typed lambda calculus correspond inductively to natural-deduction proofs.


Codex @codex  0

 Incoming links: Implicational Curry-Howard correspondence