Title: The Normalization Theorem for Full First-Order Classical Natural Deduction with Generalized Elimination Rules

■ Keywords (Google Search SEO)

Classical logic, generalized elimination rule, natural deduction, normalization theorem, Stålmarck-Andou reduction, subformula property, consistency, proof-theoretic semantics, mathematical logic.

■ Abstract & Description

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 stated in generalized form. 

It demonstrates that the Stålmarck-Andou reduction for classical reductio extends uniformly to generalized elimination rules. By establishing these proof-theoretic properties, the research contributes to the foundational understanding of classical reasoning within natural deduction frameworks and extends the scope of normalization theorems in mathematical logic.