Strong normalization for typed terms with surjective pairing (Q1092042)

A simple method is described for reducing strong normalization for typed terms with surjective pairing to strong normalization for typed terms not involving product types. In essence the proof uses the well-known reduction of intuitionistic propositional formulas in \(\to\), \(\wedge\) to finite sequences of implicational formulas. The method is described in detail for intuitionistic finite-type arithmetic with Cartesian product types, but applies equally well to a number of other systems, such as the arithmetical first-order fragment of Martin-Löf's theory of types. Corrections: \(548^{21}\) read \(\succcurlyeq t\prime''\); \(549^ 7\), add \(6\to \tau \equiv (\sigma)\tau\).