Peirce's Rule in Natural Deduction

AbstractIn stark contrast to Natural Deduction for Intuitionistic Logic, Natural Deduction for Classical Logic suffers from some well-known limitations: although normalisation can be proved, the standard proof of Prawitz (Natural deduction. A proof — Theoretical study, Almquist and Wiksell, Stockholm, 1965) is restricted to a fragment of classical predicate logic without ∨ and without ∃ due to some effects of the rule of classical negation, and a proof for classical predicate logic without ¬ and without ⊥ cannot be given; the extension of Prawitz’ proof to a language with ∨ and ∃ due to Stalmarck (J. Symbolic Logic 56 (1991) 129) still remaining language dependent on ¬ and ⊥.Such facts raise some doubts about the proof theoretical significance of the classical negation rule, the reductio ad absurdum, introduced by Prawitz. Instead of this rule, Peirce's Rule may be chosen, a purely implicative elimination rule, proposed for Classical Natural Deduction by Curry (Foundations of Mathematical Logic, McGraw-Hill, New York, 1963): this rule can be proved to be deductively equivalent with the classical negation rule, and this rule admits formulations of classical predicate logic without ¬ and without ⊥. In the following paper, it is shown that with Peirce's Rule, several theorems of weak normalisation for classical logic are provable, i.e. weak normalisation for any fragment of classical logic containing → and being enriched with any of the signs and respective rules ∧,∨,⊥,∀,∃—thus the most general proofs of normalisation for classical predicate logic are given