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

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 No keywords specified (fix it)
Categories No categories specified
(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,417
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

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Ultimate Normal Forms for Parallelized Natural Deductions.Neil Tennant - 2002 - Logic Journal of the IGPL 10 (3):299-337.
A Strong Normalization Result for Classical Logic.Franco Barbanera & Stefano Berardi - 1995 - Annals of Pure and Applied Logic 76 (2):99-116.
Identity of Proofs Based on Normalization and Generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
An Elementary Proof of Strong Normalization for Intersection Types.Valentini Silvio - 2001 - Archive for Mathematical Logic 40 (7):475-488.
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
A Mixed Λ-Calculus.Marie-Renée Fleury & Myriam Quatrini - 2007 - Studia Logica 87 (2-3):269-294.


Added to PP index

Total views
4 ( #1,245,498 of 2,449,108 )

Recent downloads (6 months)
4 ( #177,092 of 2,449,108 )

How can I increase my downloads?


Sorry, there are not enough data points to plot this chart.

My notes