Normal derivability in classical natural deduction (Q2890694)

The paper provides a normalization procedure for natural deduction systems for first-order intuitionistic, classical and some modal logics. The results are partly based on earlier works of von Plato and Negri. In contrast to other known methods, this procedure is based only on local permutation steps and does not require restrictions neither on the language of the system nor on the application of indirect proof or elimination rules. The system uses general elimination rules (with introduction of assumptions to be discharged instead of direct deduction from major premise) for all constants (not only for \(\vee \) and \(\exists \)) but it is shown that the procedure applies also to systems with standard elimination rules. Normal derivation is defined as the one where all major premises of elimination rules are assumptions. It is shown that all derivations in the considered systems convert into normal derivations, and that the latter satisfy the subformula property.NEWLINENEWLINEThe paper contains an interesting contribution to investigations on natural deduction but there is one drawback which needs to be noted. In the last section this result is extended to some system for modal logic which is called in the paper `classical modal logic'. This is misleading for two reasons. First, the name `classical' is sometimes applied to the weakest family of modal logics (instead of the name `congruent'); but the system presented in the paper certainly provides a formalization of some normal (hence much stronger) modal logic. Second, which logic is formalized by the rules depends on what we mean by `modal formulas' in the \(\square I\) rule. Following specific definitions of Prawitz we can obtain (due to \(\square E\)) either the system for S4 or for S5, but this is not stated in the text.