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

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

#### Abstract

^{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

#### Full Text:

PDF#### 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).

ISSN: 2300-9802 (electronic version)