On the proof-theory of a first-order extension of GL
DOI:
https://doi.org/10.12775/LLP.2013.030Keywords
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, aAbstract
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.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).
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 704
Number of citations: 4
