Abstract.
The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.
Through the condition that in a cut-free derivation of the sequent Γ⇒C, no inactive weakening or contraction formulas remain in Γ, a correspondence with the formal derivability relation of natural deduction is obtained: All formulas of Γ become open assumptions in natural deduction, through an inductively defined translation. Weakenings are interpreted as vacuous discharges, and contractions as multiple discharges. In the other direction, non-normal derivations translate into derivations with cuts having the cut formula principal either in both premisses or in the right premiss only.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Additional information
Received: 1 December 1998 / Revised version: 30 June 2000 / Published online: 18 July 2001
Rights and permissions
About this article
Cite this article
von Plato, J. Natural deduction with general elimination rules. Arch. Math. Logic 40, 541–567 (2001). https://doi.org/10.1007/s001530100091
Issue Date:
DOI: https://doi.org/10.1007/s001530100091