Strong normalization of classical natural deduction with disjunctions
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.
- A note on strong normalization in classical natural deduction
- Strong normalization results by translation
- A semantical proof of the strong normalization theorem for full propositional classical natural deduction
- A short proof of the strong normalization of classical natural deduction with disjunction
- A simple proof of second-order strong normalization with permutative conversions
- A semantics of realisability for the classical propositional natural deduction
- A short proof of the strong normalization of classical natural deduction with disjunction
- A simple proof of second-order strong normalization with permutative conversions
- An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
- Call-by-value is dual to call-by-name
- Church-Rosser property of a simple reduction for full first-order classical natural deduction
- Domain-free -calculus
- scientific article; zbMATH DE number 1615235 (Why is no real title available?)
- scientific article; zbMATH DE number 1696602 (Why is no real title available?)
- scientific article; zbMATH DE number 1722654 (Why is no real title available?)
- scientific article; zbMATH DE number 2185662 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- Natural deduction with general elimination rules
- Non-strictly positive fixed points for classical natural deduction
- On the strong normalisation of intuitionistic natural deduction with permutation-conversions
- Parallel reductions in \(\lambda\)-calculus
- Proofs of strong normalisation for second order classical natural deduction
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Stabilization -- an alternative to double-negation translation for classical natural deduction
- Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus
- Strong normalization proof with CPS-translation for second order classical natural deduction
- The duality of computation
- Peirce's rule in natural deduction.
- A strong normalization result for classical logic
- A simple proof of second-order strong normalization with permutative conversions
- scientific article; zbMATH DE number 1722654 (Why is no real title available?)
- Normalization theorems for full first order classical natural deduction
- scientific article; zbMATH DE number 1114347 (Why is no real title available?)
- Proofs of strong normalisation for second order classical natural deduction
- Strong normalization proof with CPS-translation for second order classical natural deduction
- A short proof of the strong normalization of classical natural deduction with disjunction
- scientific article; zbMATH DE number 1377712 (Why is no real title available?)
- scientific article; zbMATH DE number 1405618 (Why is no real title available?)
- A note on strong normalization in classical natural deduction
- Peirce's rule in a full natural deduction system
- Strong normalization for truth table natural deduction
- Classical Logic with Mendler Induction
- Proof Terms for Generalized Natural Deduction
- Strong normalization results by translation
- A semantical proof of the strong normalization theorem for full propositional classical natural deduction
- Strong normalization proofs by CPS-translations
This page was built for publication: Strong normalization of classical natural deduction with disjunctions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2482841)
