= Solution
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.
Back to article page
