A formalization of Sambins's normalization for GL

Mathematical Logic Quarterly 39 (1):133-142 (1993)
  Copy   BIBTEX


Sambin [6] 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 [1], 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



    Upload a copy of this work     Papers currently archived: 76,264

External links

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

Through your library

Similar books and articles

A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
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 Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
Identity of proofs based on normalization and generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.


Added to PP

34 (#345,596)

6 months
1 (#449,844)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Edward Haeusler
Pontifícia Universidade Católica do Rio de Janeiro

Citations of this work

No citations found.

Add more citations

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.
First-order Logic.William Craig - 1975 - Journal of Symbolic Logic 40 (2):237-238.
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.

Add more references