A cut-elimination proof in intuitionistic predicate logic
Abstract
In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.Author's Profile
Other Versions
No versions found
My notes
Similar books and articles
Sufficient conditions for cut elimination with complexity analysis.João Rasga -2007 -Annals of Pure and Applied Logic 149 (1-3):81-99.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré,Linda Postniece &Alwen Tiu -1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev,Advances in Modal Logic. CSLI Publications. pp. 43-66.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré,Linda Postniece &Alwen Tiu -1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev,Advances in Modal Logic. CSLI Publications. pp. 43-66.
An approach to infinitary temporal proof theory.Stefano Baratella &Andrea Masini -2004 -Archive for Mathematical Logic 43 (8):965-990.
A note on an alternative Gentzenization of RW+∘.Mirjana Ilić -2021 -Mathematical Logic Quarterly 67 (2):186-192.
LEt ® , LR °[^( ~ )], LK and cutfree proofs.Katalin Bimbó -2007 -Journal of Philosophical Logic 36 (5):557-570.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff &Luis Pinto -1998 -Studia Logica 60 (1):107-118.
CERES in higher-order logic.Stefan Hetzl,Alexander Leitsch &Daniel Weller -2011 -Annals of Pure and Applied Logic 162 (12):1001-1034.
Two measures for proving Gentzen's Hauptsatz without mix.Mirjana Borisavljević -2003 -Archive for Mathematical Logic 42 (4):371-387.
Analytics
Added to PP
2014-01-16
Downloads
46 (#535,220)
6 months
4 (#1,000,731)
2014-01-16
Downloads
46 (#535,220)
6 months
4 (#1,000,731)
Historical graph of downloads
How can I increase my downloads?Author's Profile
Citations of this work
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević -2006 -Archive for Mathematical Logic 45 (2):113-148.
Gentzen’s “cut rule” and quantum measurement in terms of Hilbert arithmetic. Metaphor and understanding modeled formally.Vasil Penchev -2022 -Logic and Philosophy of Mathematics eJournal 14 (14):1-37.
The Elimination of Maximum Cuts in Linear Logic and BCK Logic.Mirjana Borisavljevic -2023 -Studia Logica 111 (3):391-429.
Computing interpolants in implicational logics.Makoto Kanazawa -2006 -Annals of Pure and Applied Logic 142 (1):125-201.
References found in this work
Untersuchungen über das logische Schließen. I.Gerhard Gentzen -1935 -Mathematische Zeitschrift 35:176–210.
Untersuchungen über das logische Schließen. II.Gerhard Gentzen -1935 -Mathematische Zeitschrift 39:405–431.
The correspondence between cut-elimination and normalization.J. Zucker -1974 -Annals of Mathematical Logic 7 (1):1-112.
The correspondence between cut-elimination and normalization II.J. Zucker -1974 -Annals of Mathematical Logic 7 (2):113.
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-54b44b69b7-cj6sj uwo