Strong normalization for simply typed lambda calculus

(Tait's reducibility method.) Define, by induction on the structure of types, a set $\mathrm{RED}_A$ of "reducible terms" for every type $A$: for a base type $o$, let $\mathrm{RED}_o$ be the set $SN$ of all strongly normalizing terms; for a function type, let $\mathrm{RED}_{A\to B} = \{t : \text{for every } u \in \mathrm{RED}_A,\ t\,u \in \mathrm{RED}_B\}$.

One first proves, by induction on $A$, three technical properties together: (CR1) every term in $\mathrm{RED}_A$ is strongly normalizing; (CR2) $\mathrm{RED}_A$ is closed under $\beta$-reduction (if $t\in\mathrm{RED}_A$ and $t\to t'$ then $t'\in\mathrm{RED}_A$); (CR3) any "neutral" term (a variable or application, not an abstraction) all of whose one-step reducts already lie in $\mathrm{RED}_A$ must itself lie in $\mathrm{RED}_A$. The base case is immediate from the definition of $SN$; the function-type case unfolds the definition of $\mathrm{RED}_{A\to B}$ and uses the induction hypothesis on the smaller types $A$ and $B$.

Next, one shows every well-typed term is reducible under any substitution of reducible terms for its free variables: by induction on the typing derivation of $\Gamma \vdash t:A$, if $\sigma$ assigns each variable $x$ in $\Gamma$ a term $\sigma(x)\in\mathrm{RED}_{\Gamma(x)}$, then $t\sigma \in \mathrm{RED}_A$. The variable case is immediate. The application case follows directly from the definition of $\mathrm{RED}_{A\to B}$. The abstraction case needs the most care: for $(\lambda x.\,t)\sigma$ applied to any $u\in\mathrm{RED}_A$, the term reduces in one $\beta$-step to $t(\sigma,x{:=}u)$, which is in $\mathrm{RED}_B$ by the induction hypothesis (applied to the extended substitution); property (CR3) — closure under "expansion" for terms whose reducts are all already reducible — then places $(\lambda x.\,t)\sigma\,u$ itself in $\mathrm{RED}_B$, so $(\lambda x.\,t)\sigma \in \mathrm{RED}_{A\to B}$ by definition.

Finally, apply this to the identity substitution: every variable $x{:}A$ is itself neutral with no reducts at all, so it is vacuously in $\mathrm{RED}_A$ by (CR3). So for any closed derivation $\Gamma \vdash t:A$, taking $\sigma$ to map each $x$ to itself gives $t = t\sigma \in \mathrm{RED}_A$. By (CR1), $\mathrm{RED}_A \subseteq SN$, so $t \in SN$: every well-typed term is strongly normalizing. $\blacksquare$