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 Author
George Tourlakis York University, Department of Electrical Engineering and Computer Science Author

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 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 DOI: https://doi.org/10.2307/2274147

G. Boolos, The logic of provability, Cambridge University Press (2003), DOI: https://doi.org/10.1017/CBO9780511625183 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 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 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 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. 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 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 DOI: https://doi.org/10.1093/logcom/8.1.119

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

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 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 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 DOI: https://doi.org/10.1093/jigpal/jzl025

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

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

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

C. Smorynski, Self-Reference and Modal Logic, Springer, New York (1985), DOI: https://doi.org/10.1007/978-1-4613-8601-8 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 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 DOI: https://doi.org/10.1017/CBO9780511615566

G. Tourlakis, Mathematical Logic, John Wiley & Sons, Hoboken, NJ (2008), DOI: https://doi.org/10.1002/9781118032435 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 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.

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.

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

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 DOI: https://doi.org/10.1142/9789812776471_0001