STABILIZATION—AN ALTERNATIVE TO DOUBLE-NEGATION TRANSLATION FOR CLASSICAL NATURAL DEDUCTION
Ralph Matthes · 2006
A new proof of strong normalization of Parigot’s second-order λµ-calculus is given by a reduction-preserving embedding into system F (second-order polymorphic λ-calculus). The main idea is to use the least stable supertype for any type. These non-strictly positive inductive types and their associated iteration principle are available in system F, and allow to give a translation vaguely related to CPS translations (corresponding to Kolmogorov’s double-negation embedding of classical logic into intuitionistic logic). However, they simulate Parigot’s µ-reductions whereas CPS translations hide them. As a major advantage, this embedding does not use the idea of reducing stability (¬¬A → A) to that for atomic formulae. Therefore, it even extends to positive fixed-point types. The article expands on “Parigot’s Second-Order λµ-Calculus and Inductive Types ” (Conference Proceedings TLCA 2001, Springer LNCS 2044) by the author. 1