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

• Authors: Schwartz Yehuda , Tourlakis George
• Languages of publication: EN

Abstracts

EN

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.

Keywords

EN

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; arithmetical completeness

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2014
• Volume: 23
• Issue: 3
• Pages: 329–363

Dates

published

2014-09-01

online

2013-09-18

Contributors

author

Schwartz Yehuda

• Toronto Stn Q, P.O. Box 1204, 27 St Clair Ave E, Toronto M4T 1L0, ON, Canada

author

Tourlakis George

• Dept. of EECS, Lassonde School of Engineering, York University, 4700 Keele St., Toronto M3J 1P3, ON, Canada

References

• 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).

Identifiers

DOI

10.12775/LLP.2013.030