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

Edward Haeusler
Pontifícia Universidade Católica do Rio de Janeiro
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
Keywords mechanization of proof procedures  cut‐elimination  Sequent calculus  normalization of proofs  modal logic of provability
Categories (categorize this paper)
DOI 10.1002/malq.19930390116
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 63,360
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

First-Order Logic.Raymond M. Smullyan - 1968 - New York [Etc.]Springer-Verlag.
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

Citations of this work BETA

No citations found.

Add more citations

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 index

Total views
34 ( #318,716 of 2,448,895 )

Recent downloads (6 months)
1 ( #444,630 of 2,448,895 )

How can I increase my downloads?


My notes