Mathematical Logic Quarterly 39 (1):133-142 (1993)
AbstractSambin  proved the normalization theorem for GL, the modal logic of provability, in a sequent calculus version called by him GLS. His proof does not take into account the concept of reduction, commonly used in normalization proofs. Bellini , on the other hand, gave a normalization proof for GL using reductions. Indeed, Sambin's proof is a decision procedure which builds cut-free proofs. In this work we formalize this procedure as a recursive function and prove its recursiveness in an arithmetically formalizable way, concluding that the normalization of GL can be formalized in PA. MSC: 03F05, 03B35, 03B45
Similar books and articles
Some general results about proof normalization.Marc Aiguier & Delphine Longuet - 2010 - Logica Universalis 4 (1):1-29.
Light affine lambda calculus and polynomial time strong normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
A purely syntactic and cut-free sequent calculus for the modal logic of provability.Francesca Poggiolesi - 2009 - Review of Symbolic Logic 2 (4):593-611.
A new deconstructive logic: Linear logic.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1997 - Journal of Symbolic Logic 62 (3):755-807.
A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
On the proof-theory of a first-order extension of GL.Yehuda Schwartz & George Tourlakis - 2014 - Logic and Logical Philosophy 23 (3).
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 2008 - In Carlos Areces & Robert Goldblatt (eds.), Advances in Modal Logic, Volume 7. CSLI Publications. pp. 43-66.
Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
Added to PP
Historical graph of downloads
Citations of this work
No citations found.
References found in this work
First-Order Logic.Raymond Merrill Smullyan - 1968 - Berlin, Germany: New York [Etc.]Springer-Verlag.
The Unprovability of Consistency: An Essay in Modal Logic.George Boolos - 1979 - Cambridge, England: Cambridge University Press.
Proof Methods for Modal and Intuitionistic Logics.Melvin Fitting - 1985 - Journal of Symbolic Logic 50 (3):855-856.
The Unprovability of Consistency. An Essay in Modal Logic.C. Smoryński - 1979 - Journal of Symbolic Logic 46 (4):871-873.