An Arithmetically Complete Predicate Modal Logic

Yunge Hao; George Tourlakis

doi:10.18778/0138-0680.2021.18

Authors

Yunge Hao York University, Department of Electrical Engineering and Computer Science
George Tourlakis York University, Department of Electrical Engineering and Computer Science

DOI:

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

Keywords:

Predicate modal logic, arithmetic completeness, logic GL, Solovay's theorem, equational proofs

Abstract

This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness (with respect to finite reverse well-founded Kripke models) is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.

References

S. Artemov, G. Dzhaparidze, Finite Kripke Models and Predicate Logics of Provability, Journal of Symbolic Logic, vol. 55(3) (1990), pp. 1090–1098, DOI: https://doi.org/10.2307/2274475
Google Scholar DOI: https://doi.org/10.2307/2274475

A. Avron, On modal systems having arithmetical interpretations, Journal of Symbolic Logic, vol. 49(3) (1984), pp. 935–942, DOI: https://doi.org/10.2307/2274147
Google Scholar DOI: https://doi.org/10.2307/2274147

G. Boolos, The logic of provability, Cambridge University Press (2003), DOI: https://doi.org/10.1017/CBO9780511625183
Google Scholar DOI: https://doi.org/10.1017/CBO9780511625183

E. W. Dijkstra, C. S. Scholten, Predicate Calculus and Program Semantics, Springer, New York (1990), DOI: https://doi.org/10.1007/978-1-4612-3228-5
Google Scholar DOI: https://doi.org/10.1007/978-1-4612-3228-5

K. Fine, Failures of the interpolation lemma in quantfied modal logic, Journal of Symbolic Logic, vol. 44(2) (1979), pp. 201–206, DOI: https://doi.org/10.2307/2273727
Google Scholar DOI: https://doi.org/10.2307/2273727

F. Gao, G. Tourlakis, A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics, Bulletin of the Section of Logic, vol. 44(3/4) (2015), DOI: https://doi.org/10.18778/0138-0680.44.3.4.03
Google Scholar DOI: https://doi.org/10.18778/0138-0680.44.3.4.03

K. Gödel, Eine Interpretation des intuitionistischen Aussagenkalkuls, Ergebnisse Math, vol. 4 (1933), pp. 39–40.
Google Scholar DOI: https://doi.org/10.1007/BF01708881

D. Gries, F. B. Schneider, A Logical Approach to Discrete Math, Springer, New York (1994), DOI: https://doi.org/10.1007/978-1-4757-3837-7
Google Scholar DOI: https://doi.org/10.1007/978-1-4757-3837-7

D. Gries, F. B. Schneider, Adding the Everywhere Operator to Propositional Logic, Journal of Logic and Computation, vol. 8(1) (1998), pp. 119–129, DOI: https://doi.org/10.1093/logcom/8.1.119
Google Scholar DOI: https://doi.org/10.1093/logcom/8.1.119

D. Hilbert, W. Ackermann, Principles of Mathematical Logic, Chelsea, New York (1950).
Google Scholar

D. Hilbert, P. Bernays, Grundlagen der Mathematik I and II, Springer, New York (1968), DOI: https://doi.org/10.1007/978-3-642-86894-8
Google Scholar DOI: https://doi.org/10.1007/978-3-642-86894-8

G. Japaridze, D. de Jongh, The Logic of Provability, [in:] Buss, S. R. (ed.), Handbook of Proof Theory, Elsevier Science B.V. (1998), pp. 475–550, DOI: https://doi.org/10.1016/S0049-237X(98)80022-0
Google Scholar DOI: https://doi.org/10.1016/S0049-237X(98)80022-0

F. Kibedi, G. Tourlakis, A Modal Extension of Weak Generalisation Predicate Logic, Logic Journal of IGPL, vol. 14(4) (2006), pp. 591–621, DOI: https://doi.org/10.1093/jigpal/jzl025
Google Scholar DOI: https://doi.org/10.1093/jigpal/jzl025

S. Kleene, Introduction to metamathematics, North-Holland, Amsterdam (1952).
Google Scholar

S. A. Kripke, A completeness theorem in modal logic, Journal of Symbolic Logic, vol. 24(1) (1959), pp. 1–14, DOI: https://doi.org/10.2307/2964568
Google Scholar DOI: https://doi.org/10.2307/2964568

E. Mendelson, Introduction to Mathematical Logic, 3rd ed., Wadsworth & Brooks, Monterey, CA (1987), DOI: https://doi.org/10.1007/978-1-4615-7288-6
Google Scholar DOI: https://doi.org/10.1007/978-1-4615-7288-6

F. Montagna, The predicate modal logic of provability, Notre Dame Journal of Formal Logic, vol. 25(2) (1984), pp. 179–189, DOI: https://doi.org/10.1305/ndjfl/1093870577
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093870577

Y. Schwartz, G. Tourlakis, On the Proof-Theory of two Formalisations of Modal First-Order Logic, Studia Logica, vol. 96(3) (2010), pp. 349–373, DOI: https://doi.org/10.1007/s11225-010-9294-y
Google Scholar DOI: https://doi.org/10.1007/s11225-010-9294-y

Y. Schwartz, G. Tourlakis, On the proof-theory of a first-order extension of GL, Logic and Logical Philosophy, vol. 23(3) (2013), pp. 329–363, DOI: https://doi.org/10.12775/llp.2013.030
Google Scholar DOI: https://doi.org/10.12775/LLP.2013.030

Y. Schwartz, G. Tourlakis, A proof theoretic tool for first-order modal logic, Bulletin of the Section of Logic, vol. 42(3/4) (2013), pp. 93–110.
Google Scholar

J. R. Shoenfield, Mathematical Logic, Addison-Wesley, Reading, MA (1967).
Google Scholar

C. Smorynski, Self-Reference and Modal Logic, Springer, New York (1985), DOI: https://doi.org/10.1007/978-1-4613-8601-8
Google Scholar DOI: https://doi.org/10.1007/978-1-4613-8601-8

R. M. Solovay, Provability interpretations of modal logic, Israel Journal of Mathematics, vol. 25(3–4) (1976), pp. 287–304, DOI: https://doi.org/10.1007/bf02757006
Google Scholar DOI: https://doi.org/10.1007/BF02757006

G. Tourlakis, Lectures in Logic and Set Theory, Volume 1: Mathematical Logic, Cambridge University Press, Cambridge (2003), DOI: https://doi.org/10.1017/CBO9780511615559
Google Scholar DOI: https://doi.org/10.1017/CBO9780511615566

G. Tourlakis, Mathematical Logic, John Wiley & Sons, Hoboken, NJ (2008), DOI: https://doi.org/10.1002/9781118032435
Google Scholar DOI: https://doi.org/10.1002/9781118032435

G. Tourlakis, A new arithmetically incomplete first-order extension of GL all theorems of which have cut free proofs, Bulletin of the Section of Logic, vol. 45(1) (2016), pp. 17–31, DOI: https://doi.org/10.18778/0138-0680.45.1.02
Google Scholar DOI: https://doi.org/10.18778/0138-0680.45.1.02

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

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

V. A. Vardanyan, Arithmetic complexity of predicate logics of provability and their fragments, Soviet Mathematics Doklady, vol. 34 (1986), pp. 384–387, URL: http://mi.mathnet.ru/eng/dan8607
Google Scholar

R. E. Yavorsky, On Arithmetical Completeness of First-Order Logics of Provability, Advances in Modal Logic, (2002), pp. 1–16, DOI: https://doi.org/10.1142/9789812776471_0001
Google Scholar DOI: https://doi.org/10.1142/9789812776471_0001