We introduce a first order extension of GL, called ML 3 , and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML 3 , as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove that ML 3 is sound with respect to arithmetical interpretations and that it is also sound and complete with respect to converse well-founded and transitive finite Kripke models. This leads us to expect that a Solovay-like proof of arithmetical completeness of ML 3 is possible.
Keywords provability logic  GL  Hilbert-style logic  a  modal first-order logic  reflection theorem  Gentzen-style logic  arithmetical interpretation  cut-elimination  sequent calculus  soundness
Categories (categorize this paper)
DOI 10.12775/LLP.2013.030
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: 65,784
Through your library

References found in this work BETA

A Completeness Theorem in Modal Logic.Saul A. Kripke - 1959 - Journal of Symbolic Logic 24 (1):1-14.
The Modal Logic of Provability. The Sequential Approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.
On Modal Systems Having Arithmetical Interpretations.Arnon Avron - 1984 - Journal of Symbolic Logic 49 (3):935-942.
Failures of the Interpolation Lemma in Quantified Modal Logic.Kit Fine - 1979 - Journal of Symbolic Logic 44 (2):201-206.
The Modal Logic of Provability: Cut-Elimination. [REVIEW]Silvio Valentini - 1983 - Journal of Philosophical Logic 12 (4):471 - 476.

View all 12 references / Add more references

Citations of this work BETA

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.
Realization of Intuitionistic Logic by Proof Polynomials.Sergei N. Artemov - 1999 - Journal of Applied Non-Classical Logics 9 (2-3):285-301.
A Cut-Free Gentzen Formulation of Basic Propositional Calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
Predicate Logics on Display.Heinrich Wansing - 1999 - Studia Logica 62 (1):49-75.
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
20 ( #544,953 of 2,463,156 )

Recent downloads (6 months)
1 ( #449,391 of 2,463,156 )

How can I increase my downloads?


My notes