A simple proof of second-order strong normalization with permutative conversions

DOI10.1016/J.APAL.2005.05.009MaRDI QIDQ2566069zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta, G. E. Mints

Publication date 22 September 2005

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.009

zbMATH Keywords

permutative conversions second-order natural deduction strong normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Review text

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).

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

Uses Software

Automath

This page was built for publication: A simple proof of second-order strong normalization with permutative conversions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2566069)