A proof of Gentzen's Hauptsatz without multicut
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.Author's Profile
Other Versions
No versions found
My notes
Similar books and articles
Gentzen’s consistency proof without heightlines.Annika Siders -2013 -Archive for Mathematical Logic 52 (3-4):449-468.
Two measures for proving Gentzen's Hauptsatz without mix.Mirjana Borisavljević -2003 -Archive for Mathematical Logic 42 (4):371-387.
The Hauptsatz for Stratified Comprehension: A Semantic Proof.Marcel Crabbé -1994 -Mathematical Logic Quarterly 40 (4):481-489.
Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction.Jan von Plato &Sara Negri -2016 - In Peter Schuster & Dieter Probst,Concepts of Proof in Mathematics, Philosophy, and Computer Science. Boston: De Gruyter. pp. 269-290.
A cut-elimination proof in intuitionistic predicate logic.Mirjana Borisavljević -1999 -Annals of Pure and Applied Logic 99 (1-3):105-136.
A Nonconstructive Proof of Gentzen's Hauptsatz for Second Order Predicate Logic.W. W. Tait -1968 -Journal of Symbolic Logic 33 (2):289-290.
Analyticity, Balance and Non-admissibility of Cut in Stoic Logic.Susanne Bobzien &Roy Dyckhoff -2018 -Studia Logica 107 (2):375-397.
Tait W. W.. A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic. Bulletin of the American Mathematical Society, vol. 72 , pp. 980–983. [REVIEW]Moto-O. Takahashi -1968 -Journal of Symbolic Logic 33 (2):289-290.
Analytics
Added to PP
2013-11-23
Downloads
70 (#329,859)
6 months
11 (#343,540)
2013-11-23
Downloads
70 (#329,859)
6 months
11 (#343,540)
Historical graph of downloads
How can I increase my downloads?Author's Profile
Citations of this work
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.
Sequent calculus in natural deduction style.Sara Negri &Jan von Plato -2001 -Journal of Symbolic Logic 66 (4):1803-1816.
A sequent calculus isomorphic to gentzen’s natural deduction.Jan von Plato -2011 -Review of Symbolic Logic 4 (1):43-53.
References found in this work
The collected papers of Gerhard Gentzen.Gerhard Gentzen -1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.
Proof theory.Gaisi Takeuti -1987 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Home |New books and articles |Bibliographies |Philosophy journals |About PhilPapers |API |Contact us |Code of conduct
PhilPapers logo byAndrea Andrews andMeghan Driscoll.
This site uses cookies and Google Analytics (see ourterms & conditions for details regarding the privacy implications).Use of this site is subject toterms & conditions.
All rights reserved byThe PhilPapers Foundation
Server: philpapers-web-5b9ff6f457-ljglp uwo