Curry–Howard correspondence

(Proofs become programs.) By induction on a natural-deduction derivation of $\vdash \varphi$. If the last rule is $\to$-introduction, deriving $\varphi=\psi\to\chi$ from a subproof of $\chi$ under hypothesis $\psi$: by the induction hypothesis that subproof translates to a term $t$ with $x{:}A_\psi \vdash t : A_\chi$ (the hypothesis becomes a free variable $x$); then $\lambda x{:}A_\psi.\,t$ is closed and has type $A_\psi\to A_\chi=A_\varphi$. If the last rule is $\to$-elimination (modus ponens) from $\psi\to\chi$ and $\psi$: by the induction hypothesis we have terms $t_1 : A_\psi\to A_\chi$ and $t_2 : A_\psi$; then $t_1\,t_2 : A_\chi$. The $\wedge$-introduction and $\wedge$-elimination rules translate symmetrically to pairing $\langle t_1,t_2\rangle$ and the two projections. Every rule of the proof system has a matching term-building rule, so induction on the derivation produces a well-typed closed term of type $A_\varphi$.

(Programs become proofs.) Conversely, by induction on a typing derivation $\vdash t : A$. Each typing rule — variable, abstraction, application, pairing, projection — has exactly the same tree shape as a natural-deduction rule — hypothesis, $\to$-introduction, $\to$-elimination, $\wedge$-introduction, $\wedge$-elimination. So take the same derivation tree, erase all the terms, and read each type as the formula it translates from: this is precisely a valid intuitionistic proof of $\varphi$ (where $A=A_\varphi$).

Since the two translations (proof $\to$ term, and term $\to$ proof) are structural inverses of each other on derivation trees — each one undoes exactly what the other does, rule by rule — $\varphi$ is provable exactly when $A_\varphi$ is inhabited. $\blacksquare$