On the proof-theory of a first-order extension of GL

Yehuda Schwartz, George Tourlakis

DOI: http://dx.doi.org/10.12775/LLP.2013.030


We introduce a first order extension of GL, called ML3, 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 ML3, as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove that ML3 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 ML3 is possible.


Gentzen-style logic; Gentzen’s Hauptsatz; Hilbert-style logic; GL; K4; provability logic; provability predicate; modal first-order logic; sequent calculus; cut-elimination; reflection theorem; Craig interpolation; arithmetical interpretation; soundness; a

Full Text:



Avron, A., “On modal systems having arithmetical interpretations”, Journal of Symbolic Logic, 49 (1984), 3: 935–942. DOI: 10.2307/2274147

Boolos, G., The Logic of Provability, Cambridge University Press, Cambridge, 1993.

Fine, K., “Failures of the interpolation lemma in quantified modal logic”, Journal of Symbolic Logic, 44 (1979), 2: 201–206. DOI: 10.2307/2273727

Fitting, M., and R.L. Mendelsohn, First-Order Modal Logic, Kluwer Academic Publishers, Dordrecht, 1998.

Gries, D., and F.B. Schneider, “Adding the everywhere operator to propositional logic”, Journal Logic Computat., 8 (1998), 1: 119–129. DOI: 10.1093/logcom/8.1.119

Kibedi, F., and G. Tourlakis, “A modal extension of weak generalization predicate logic”, Logic Journal of the IGPL, 14 (2006), 4: 591–621.

Kripke, S.A., “A completeness theorem in modal logic”, Journal of Symbolic Logic, 24 (1959): 1–14. DOI: 10.1093/jigpal/jzl025

Leivant, D., “On the proof theory of the modal logic for arithmetic provability”, Journal of Symbolic Logic, 46 (1981), 3: 531–538. DOI: 10.2307/2273755

Mendelson, E., Introduction to Mathematical Logic, 3rd edition, Wadsworth & Brooks, Monterey, California, 1987.

Montagna, F., “The predicate modal logic of provability”, Notre Dame Journal of Formal Logic, 25 (1984): 179–189. DOI: 10.1305/ndjfl/1093870577

Sambin, G., and S. Valentini, “A modal sequent calculus for a fragment of arithmetic”, Studia Logica, 39 (1980), 2/3: 245–256. DOI: 10.1007/BF00370323

Sambin, G., and S. Valentini, “The modal logic of provability. The sequential approach”, Journal of Philosophical Logic, 11 (1982), 3: 311–342. DOI: 10.1007/BF00293433

Sasaki, K., “Löb’s axiom and cut-elimination theorem”, Academia Mathematical Sciences and Information Engineering Nanzan University, 1 (2001): 91–98.

Schütte, K., Proof Theory, Springer-Verlag, New York, 1977.

Schwartz, Y., and G. Tourlakis, “On the proof-theory of two formalisations of modal first-order logic”, Studia Logica, 96 (2010), 3: 349–373. DOI: 10.1007/s11225-010-9294-y

Shoenfield, J.R., Mathematical Logic, Addison-Wesley, Reading, Massachusetts, 1967.

Smoryński, C., Self-Reference and Modal Logic, Springer-Verlag, New York, 1985.

Takeuti, G., Proof Theory, North-Holland, Amsterdam, 1975.

Tourlakis, G., Lectures in Logic and Set Theory; Volume 1: Mathematical Logic, Cambridge University Press, Cambridge, 2003.

Tourlakis, G., and F. Kibedi, “A modal extension of first order classical logic. Part I, Bulletin of the Section of Logic, 32 (2003), 4: 165–178. PDF

Tourlakis, G., and F. Kibedi, “A modal extension of first order classical logic. Part II”, Bulletin of the Section of Logic, 33 (2004), 1: 1–10. PDF

Valentini, S., “The modal logic of provability. Cut-elimination”, Journal of Philosophical Logic, 12 (1983), 4: 471–476. DOI: 10.1007/BF00249262

Vardanyan, V.A., “On the predicate logic of provability”, preprint of the Scientific Council on the Complexity Problem “Cybernetics”, Academy of Sciences of the USSR (1985, in Russian).

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism