Natural deduction with general elimination rules

Archive for Mathematical Logic 40 (7):541-567 (2001)
  Copy   BIBTEX

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

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,353

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A normalizing system of natural deduction for intuitionistic linear logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Translations from natural deduction to sequent calculus.Jan von Plato - 2003 - Mathematical Logic Quarterly 49 (5):435.
Sequent calculus in natural deduction style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.
Normal derivations and sequent derivations.Mirjana Borisavljevi - 2008 - Journal of Philosophical Logic 37 (6):521 - 548.
Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
Normal derivability in modal logic.Jan von Plato - 2005 - Mathematical Logic Quarterly 51 (6):632-638.

Analytics

Added to PP
2013-11-23

Downloads
82 (#215,696)

6 months
15 (#174,628)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jan Von Plato
University of Helsinki

References found in this work

Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.
Die Widerspruchsfreiheit der reinen Zahlentheorie.Gerhard Gentzen - 1936 - Journal of Symbolic Logic 1 (2):75-75.

Add more references