A proof of Gentzen's Hauptsatz without multicut

Archive for Mathematical Logic 40 (1):9-18 (2001)
  Copy   BIBTEX

Abstract

Gentzen's original proof of the Hauptsatz used a rule of multicut in the case that the right premiss of cut was derived by contraction. Cut elimination is here proved without multicut, by transforming suitably the derivation of the premiss of the contraction.

Categories

Keywords

Reprint years

DOI

10.1007/s001530050170

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,202

External links

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

Through your library

My notes

Similar books and articles

Gentzen’s consistency proof without heightlines.Annika Siders - 2013 - Archive for Mathematical Logic 52 (3-4):449-468.
Review: W. W. Tait, A Nonconstructive Proof of Gentzen's Hauptsatz for Second Order Predicate Logic. [REVIEW]Moto-O. Takashaih - 1968 - Journal of Symbolic Logic 33 (2):289-290.
Two measures for proving Gentzen's Hauptsatz without mix.Mirjana Borisavljević - 2003 - Archive for Mathematical Logic 42 (4):371-387.
On the proof-theory of a first-order extension of GL.Yehuda Schwartz & George Tourlakis - 2014 - Logic and Logical Philosophy 23 (3).
Gentzen's Hauptsatz for the systems NI and NK.Andrés Raggio - 1965 - Logique Et Analyse 8:91-100.
A generalization of the Gentzen Hauptsatz.Luis E. Sanchis - 1971 - Notre Dame Journal of Formal Logic 12 (4):499-504.
The Hauptsatz for Stratified Comprehension: A Semantic Proof.Marcel Crabbé - 1994 - Mathematical Logic Quarterly 40 (4):481-489.
Gentzen's Proof of Normalization for Natural Deduction.Jan von Plato & G. Gentzen - 2008 - Bulletin of Symbolic Logic 14 (2):240 - 257.
Gentzen formulations of two positive relevance logics.Aleksandar Kron - 1980 - Studia Logica 39 (4):381 - 403.
Gentzen formulations of two positive relevance logics.Aleksandar Kron - 1981 - Studia Logica 40 (3):381 - 403.
Gödel's reformulation of Gentzen's first consistency proof for arithmetic: The no-counterexample interpretation.W. W. Tait - 2005 - Bulletin of Symbolic Logic 11 (2):225-238.
LEt ® , LR °[^( ~ )], LK and cutfree proofs.Katalin Bimbó - 2007 - Journal of Philosophical Logic 36 (5):557-570.
Reflective knowledge in the best circles.Ernest Sosa - 1997 - Journal of Philosophy 94 (8):410-430.

Analytics

Added to PP
2013-11-23

Downloads
49 (#309,238)

6 months
10 (#213,340)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Jan Von Plato
University of Helsinki

Citations of this work

Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
Gentzen's proof systems: byproducts in a work of genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Proof-theoretic pluralism.Filippo Ferrari & Eugenio Orlandelli - 2019 - Synthese 198 (Suppl 20):4879-4903.
Structural proof theory for first-order weak Kleene logics.Andreas Fjellstad - 2020 - Journal of Applied Non-Classical Logics 30 (3):272-289.
Sequent calculus in natural deduction style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.

View all 13 citations / Add more citations

References found in this work

Proof theory.Gaisi Takeuti - 1975 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.

Add more references