Strong normalization of classical natural deduction with disjunctions (Q2482841)

In \(\lambda\mu\)-calculus, a vacuous \(\mu\)-term, namely \(\mu aM\) with no occurrence of \(a\) in \(M\), causes trouble, which the authors call erasing-continuation, in connexion with CPS-translation. (`CPS' is for `continuation passing style'.) This difficulty was overlooked by \textit{P. de Groote} in his article [``Strong normalization of classical natural deduction with disjunction'', Lect. Notes Comput. Sci. 2044, 182--196 (2001; Zbl 0981.03027)], and so his proof of strong normalization is incomplete. To overcome the difficulty, the authors use the device of augmentations which they introduced in a previous paper [J. Symb. Log. 68, No. 3, 851--859 (2003); Corrigendum ibid. 68, No. 4, 1415--1416 (2003; Zbl 1058.03060)]. To a term \(M\), a set, \(\text{Aug}(M)\), of non-vacuous terms are associated in such a way that any reduction of \(M\) is simulated by terms in \(\text{Aug}(M)\) while avoiding erasure of continuation. Thus, in this paper, the authors complete a proof of strong normalization of the \(\lambda\mu\)-calculus with \(\rightarrow\), \(\wedge\), \(\vee\), and \(\perp\). They extend the strong normalization proof to the calculus that incorporates general elimination rules of \textit{J. von Plato} [Arch. Math. Logic 40, No. 7, 541--567 (2001; Zbl 1021.03050)]. \{The authors' citation `Annals of\hbox{\dots'} is in error.\} This calculus allows permutative conversions and thus provides the sub-formula property.