Normalization and excluded middle. I (Q583185)

The rule \[ \supset K:\quad \Gamma,\quad \neg A\vdash A\quad \to \quad \Gamma \vdash A \] is precisely strong enough to give classical logic from intuitionistic logic, and thus it is exactly equivalent to the law of the excluded middle. This rule is a special case of the rule: \[ \neg D:\quad \Gamma,\quad A\supset B\vdash A\quad \to \quad \Gamma \vdash A. \] The main result of the paper is to prove the normalization theorem for deductions in the propositional logics and first order predicate logics obtained from intuitionistic logic or minimal logic by adding one of these rules. Every deduction in these logics is shown to be reducible by complete \(\supset K\)-reductions to a \(\supset K\)-reduced deduction with the same undischarged assumptions and the same conclusion; and then, any \(\supset K\)-reduced deduction can be normalized by the methods used for intuitionistically based logic since each \(\supset K\)-reduced deduction has at most one inference by the rule \(\supset K\) and that, if it occurs, is at the end of the deduction.