Natural deduction with general elimination rules |
| |
Authors: | Jan von Plato |
| |
Institution: | (1) University of Helsinki, Department of Philosophy, 00014 University of Helsinki, Finland. e-mail: vonplato@helsinki.fi, FI |
| |
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.
Received: 1 December 1998 / Revised version: 30 June 2000 / Published online: 18 July 2001 |
| |
Keywords: | Mathematics Subject Classification (2000): 03F05 |
本文献已被 SpringerLink 等数据库收录! |
|