This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.

We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.

We prove the strong normalization of full classical natural deduction by using a translation into the simply typed λμ-calculus. We also extend Mendler’s result on recursive equations to this system.

In this paper, we present the -calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church–Rosser property of this system is proved using the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.

Termination for classical natural deduction is difficult in the presence of commuting/permutative conversions for disjunction. An approach based on reducibility candidates is presented that uses non-strictly positive inductive definitions.It covers second-order universal quantification and also the extension of the logic with fixed points of non-strictly positive operators, which appears to be a new result.Finally, the relation to Parigot’s strictly positive inductive definition of his set of reducibility candidates and to his notion of generalized reducibility candidates is explained.