A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs

George Tourlakis

doi:10.18778/0138-0680.45.1.02

Authors

George Tourlakis

DOI:

https://doi.org/10.18778/0138-0680.45.1.02

Keywords:

Modal logic, GL, first-order logic, proof theory, cut elimination, reflection property, disjunction property, quantified modal logic, QGL, arithmetical completeness

Abstract

Reference [12] introduced a novel formula to formula translation tool (“formula-tors”) that enables syntactic metatheoretical investigations of first-order modallogics, bypassing a need to convert them first into Gentzen style logics in order torely on cut elimination and the subformula property. In fact, the formulator tool,as was already demonstrated in loc. cit., is applicable even to the metatheoreticalstudy of logics such as QGL, where cut elimination is (provably, [2]) unavailable. This paper applies the formulator approach to show the independence of the axiom schema ☐A → ☐∀ A of the logics M³and ML³of [17, 18, 11, 13]. This leads to the conclusion that the two logics obtained by removing this axiom are incomplete, both with respect to their natural Kripke structures and to arithmetical interpretations. In particular, the so modified ML³ is, similarly to QGL, an arithmetically incomplete first-order extension of GL, but, unlike QGL, all its theorems have cut free proofs. We also establish here, via formulators, a stronger version of the disjunction property for GL and QGL without going through Gentzen versions of these logics (compare with the more complexproofs in [2,8]).

References

[1] S. Artemov and G. Dzhaparidze, Finite Kripke Models and Predicate Logics of Provability, J. of Symb. Logic 55 (1990), no. 3, pp. 1090–1098.
Google Scholar

[2] A. Avron, On modal systems having arithmetical interpretations, J. of Symb. Logic 49 (1984), no. 3, pp. 935–942.
Google Scholar

[3] G. Boolos, The Logic of Provability, Cambridge University Press, Cambridge, 1993.
Google Scholar

[4] N. Bourbaki, Éléments de Mathématique; Théorie des Ensembles, Hermann, Paris, 1966.
Google Scholar

[5] H. B. Enderton, A mathematical introduction to logic, Academic Press, New York, 1972.
Google Scholar

[6] F. Kibedi and G. Tourlakis, A modal extension of weak generalisation predicate logic, Logic Journal of the IGPL 14 (2006), no. 4, pp. 591–621.
Google Scholar

[7] F. Montagna, The predicate modal logic of provability, Notre Dame J. of Formal Logic 25 (1984), pp. 179–189.
Google Scholar

[8] G. Sambin and S. Valentini, A Modal Sequent Calculus for a Fragment of Arithmetic, Studia Logica 39 (1980), no. 2/3, pp. 245–256.
Google Scholar

[9] G. Sambin and S. Valentini, The Modal Logic of Provability. The Sequential Approach, Journal of Philosophical Logic 11 (1982), no. 3, pp. 311–342.
Google Scholar

[10] K. Schütte, Proof Theory, Springer-Verlag, New York, 1977.
Google Scholar

[11] Y. Schwartz and G. Tourlakis, On the proof-theory of two formalisations of modal first-order logic, Studia Logica 96 (2010), no. 3, pp. 349–373.
Google Scholar

[12] Y. Schwartz and G. Tourlakis, A Proof Theoretic Tool for First-Order Modal Logic, Bulletin of the Section of Logic 42 (2013), no. 3–4, pp. 93–110.
Google Scholar

[13] Y. Schwartz and G. Tourlakis, On the Proof-Theory of a First-Order Version of GL, J. of Logic and Logical Philosophy 23 (2014), no. 3, pp. 329–363.
Google Scholar

[14] J. R. Shoenfield, Mathematical Logic, Addison-Wesley, Reading, Massachusetts, 1967.
Google Scholar

[15] C. Smoryński, Self-Reference and Modal Logic, Springer-Verlag, New York, 1985.
Google Scholar

[16] G. Tourlakis, Lectures in Logic and Set Theory; Volume 1: Mathematical Logic, Cambridge University Press, Cambridge, 2003.
Google Scholar

[17] G. Tourlakis and F. Kibedi, A modal extension of first order classical logic – Part I, Bulletin of the Section of Logic 32 (2003), no. 4, pp. 165–178.
Google Scholar

[18] G. Tourlakis and F. Kibedi, A modal extension of first order classical logic – Part II, Bulletin of the Section of Logic 33 (2004), no. 1, pp. 1–10.
Google Scholar

[19] V. A. Vardanyan, On the predicate logic of provability, “Cybernetics”, Academy of Sciences of the USSR (in Russian) (1985).
Google Scholar

[20] R. E. Yavorsky, On arithmetical completeness of first-order logics, Advances in Modal Logic (F. Wolter H. Wansing M. de Rijke and M. Zakharyaschev, ed.), vol. 3, CSLI Publications, Stanford University, Stanford, USA, 2001, pp. 1–16.
Google Scholar