Journal of Symbolic Logic 66 (4):1803-1816 (2001)
Authors |
|
Abstract |
A sequent calculus is given in which the management of weakening and contraction is organized as in natural deduction. The latter has no explicit weakening or contraction, but vacuous and multiple discharges in rules that discharge assumptions. A comparison to natural deduction is given through translation of derivations between the two systems. It is proved that if a cut formula is never principal in a derivation leading to the right premiss of cut, it is a subformula of the conclusion. Therefore it is sufficient to eliminate those cuts that correspond to detour and permutation conversions in natural deduction.
|
Keywords | No keywords specified (fix it) |
Categories | (categorize this paper) |
DOI | 10.2307/2694976 |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
The Collected Papers of Gerhard Gentzen.K. Schütte - 1972 - Journal of Symbolic Logic 37 (4):752-753.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.
A Proof of Gentzen's Hauptsatz Without Multicut.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (1):9-18.
Citations of this work BETA
Harmony in Multiple-Conclusion Natural-Deduction.Nissim Francez - 2014 - Logica Universalis 8 (2):215-259.
Translations Between Gentzen–Prawitz and Jaśkowski–Fitch Natural Deduction Proofs.Shawn Standefer - 2019 - Studia Logica 107 (6):1103-1134.
Natural Deduction Systems for Nelson's Paraconsistent Logic and its Neighbors.Norihiro Kamide - 2005 - Journal of Applied Non-Classical Logics 15 (4):405-435.
Combinatorial Analysis of Proofs in Projective and Affine Geometry.Jan von Plato - 2010 - Annals of Pure and Applied Logic 162 (2):144-161.
View all 9 citations / Add more citations
Similar books and articles
Normal Derivations and Sequent Derivations.Mirjana Borisavljevi - 2008 - Journal of Philosophical Logic 37 (6):521 - 548.
The Deduction Rule and Linear and Near-Linear Proof Simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
A Speech Act Calculus. A Pragmatised Natural Deduction Calculus and its Meta-Theory.Moritz Cordes & Friedrich Reinmuth - manuscript
The Geometry of Non-Distributive Logics.Greg Restall & Francesco Paoli - 2005 - Journal of Symbolic Logic 70 (4):1108 - 1126.
Analytics
Added to PP index
2009-01-28
Total views
252 ( #43,517 of 2,505,611 )
Recent downloads (6 months)
1 ( #416,705 of 2,505,611 )
2009-01-28
Total views
252 ( #43,517 of 2,505,611 )
Recent downloads (6 months)
1 ( #416,705 of 2,505,611 )
How can I increase my downloads?
Downloads