+\newcommand{\lcfix}[2]{\mathsf{fix} \appspace #1. #2}
+
+This makes the STLC Turing incomplete. We can recover the ability to loop by
+adding a combinator that recurses:
+\begin{equation*}
+ \termt ::= \dots \separ \lcfix{x : \tya}{\termt}
+\end{equation*}
+\begin{equation*}
+ \lcfix{x : \tya}{\termt} \bred \termt[(\lcfix{x : \tya}{\termt}) / x]
+\end{equation*}
+\begin{center}
+ \begin{prooftree}
+ \AxiomC{$\Gamma,x : \tya \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
+ \end{prooftree}
+\end{center}
+
+However, we will keep STLC without such a facility. In the next section we shall
+see why that is preferable for our needs.
+
+\subsection{The Curry-Howard correspondence}
+
+It turns out that the STLC can be seen a natural deduction system. Terms are
+proofs, and their types are the propositions they prove. This remarkable fact
+is known as the Curry-Howard isomorphism.
+
+The ``arrow'' ($\to$) type corresponds to implication. If we wished to
+prove that $(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tyc
+\tyarr \tyc)$, all we need to do is to devise a $\lambda$-term that has the
+correct type:
+\begin{equation*}
+ \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
+\end{equation*}
+That is, function composition. We might want extend our bare lambda calculus
+with a couple of terms to make our natural deduction more pleasant to use. For
+example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
+are conjunctions. We also want to be able to express falsity, and that is done
+by introduced a type ``inhabited'' by no terms. If evidence of such a type is
+presented, then we can derive any type, which expresses absurdity.
+
+\newcommand{\lcinl}{\mathsf{inl}\appspace}
+\newcommand{\lcinr}{\mathsf{inr}\appspace}
+\newcommand{\lccase}[3]{\mathsf{case}\appspace#1\appspace#2\appspace#3}
+\newcommand{\lcfst}{\mathsf{fst}\appspace}
+\newcommand{\lcsnd}{\mathsf{snd}\appspace}
+\newcommand{\orint}{\vee I_{1,2}}
+\newcommand{\orintl}{\vee I_{1}}
+\newcommand{\orintr}{\vee I_{2}}
+\newcommand{\orel}{\vee E}
+\newcommand{\andint}{\wedge I}
+\newcommand{\andel}{\wedge E_{1,2}}
+\newcommand{\botel}{\bot E}
+\newcommand{\lcabsurd}{\mathsf{absurd}\appspace}