+\section{G\"odel system T}
+We shall use a variant of system T with three atomic types $\N$ (natural
+numbers), $\B$ (booleans) and $\one$ (a terminal object), and two binary
+type constructors $\times$ (product) and $\to$ (arrow type).
+
+The terms of the language comprise the usual simply typed lambda terms
+with explicit pairs, plus the following additional constants:
+\begin{itemize}
+\item $*:\one$,
+\item $true: \B$, $false:\B$, $D:A\to A \to \B \to A$
+\item $O:\N$, $S:\N \to \N$, $R:A \to (A \to \N \to A) \to \N \to A$,
+\end{itemize}
+Redexes comprise $\beta$-reduction
+\[(\beta)\;\; \lambda x:U.M \; N \leadsto M[N/x]\]
+projections
+
+\[(\pi_1)\;\;fst \pair{M}{N} \leadsto M\\ \hspace{.6cm} (\pi_2)\;\; snd \pair{M}{N}
+\leadsto N \]
+and the following type specific reductions:
+\[(D_{true})\;\;\\D\;M\;N\; true \leadsto M \hspace{.6cm}
+ (D_{false})\;\; D\;M\;N\;false \leadsto N \]
+\[(R_0)\;\;\\R\;M\;F\; 0 \leadsto M \hspace{.6cm}
+ (R_S)\;\; R\;M\;F\;(S\;n) \leadsto F\;n\;(R\;M\;F\;n) \]
+\[(*)\;\; M \leadsto * \]
+where (*) holds for any $M$ of type $\one$.
+