The Normalization Theorem for Full First-Order Classical Natural Deduction with Generalized Elimination Rules
This paper proves weak normalization, a restricted subformula property, and consistency for a full first-order classical natural deduction system in which the elimination rules for all logical connectives and quantifiers are formulated in generalized form. While normalization for classical logic and generalized rules have been studied independently, an explicit and concrete proof using Gentzen–Prawitz’s natural deduction for a full classical first-order system with generalized elimination rules has not yet been presented. This paper fills this gap by demonstrating that the St\aa{}lmarck–Andou reduction for classical reductio extends uniformly to generalized elimination rules. By separating standard introduction-elimination redexes, maximal segments generated by generalized eliminations, and classical redexes, normal derivations are shown to satisfy a restricted subformula property. Consistency follows directly from normalization and the branch analysis of closed normal derivations.
한국논리학회
한림대학교 인문학부 최승락
