A simple proof of second-order strong normalization with permutative conversions (Q2566069): Difference between revisions

The authors present a proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions. It follows the Tait-Girard approach using computability predicates and saturated sets. As main technical advantage compared with other strong normalization proofs in this area, the authors (re)establish a convenient modularity of the proof (p.~135f): ``Instead of natural deductions deriving a formula \(A\) one works (via Curry-Howard isomorphism) with corresponding \(\lambda\)-terms of type \(A\). A useful device introduced in [\textit{W. W. Tait}, ``A realizability interpretation of the theory of species'', Logic Colloq., Symp. Logic Boston 1972--73, Lect. Notes Math. 453, 240--251 (1975; Zbl 0328.02014)], [...] is to switch to untyped \(\lambda\)-terms, some of which can belong to a set \(\bar{A}\) of computable terms of type \(A\). [... A] simple induction on \(A\) proves that all terms in \(\bar{A}\) are strongly normalizing. After this it turned out to be possible to prove that every typed term \(t\) of type \(A\) belongs to \(\bar{A}\), hence strongly normalizes. The second proof is by induction on the term \(t\). [...] Most of the obvious attempts to define sets \(\overline{\exists x A}\) and \(\overline{A \vee B}\) of computable terms of type \(\exists x A\) and \(A \vee B\) stall because the complexity of the conclusion \(C\) of the \(\exists\)- or \(\vee\)-elimination rule [...] is not connected in any way with the complexity of \(\exists x A\) or \(A \vee B\). This difficulty is resolved in the present paper by additional conversions \((\exists)\), \((\vee 1)\), \((\vee 2)\) [...], which allow us to define \(\overline{\exists x A}\) in terms of \(\bar{A}\).'' The paper gives not only a simple and complete proof of strong normalization for various first- and second-order logics, but the proof is also ``suitable both for extensions to stronger systems and for teaching'' (p.~135).