Geodesic
An Arithmetically Complete Predicate Modal Logic
Bulletin of the Section of Logic, Tome 50 (2021) no. 4, pp. 513-541.

Voir la notice de l'article provenant de la source Library of Science

This paper investigates a first-order extension of GL called ^3. We outline briefly the history that led to ^3, its key properties and some of its toolbox: the 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 ^3 is arithmetically complete. As expanded below, ^3 is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"" simulating the the informal classical "⊢"―is also arithmetically complete in the Solovay sense.
Keywords: Predicate modal logic, arithmetic completeness, logic GL, Solovay's theorem, equational proofs 
@article{BSL_2021_50_4_a3,
     author = {Hao, Yunge and Tourlakis, George},
     title = {An {Arithmetically} {Complete} {Predicate} {Modal} {Logic}},
     journal = {Bulletin of the Section of Logic},
     pages = {513--541},
     publisher = {mathdoc},
     volume = {50},
     number = {4},
     year = {2021},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2021_50_4_a3/}
}
TY  - JOUR
AU  - Hao, Yunge
AU  - Tourlakis, George
TI  - An Arithmetically Complete Predicate Modal Logic
JO  - Bulletin of the Section of Logic
PY  - 2021
SP  - 513
EP  - 541
VL  - 50
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2021_50_4_a3/
LA  - en
ID  - BSL_2021_50_4_a3
ER  - 
%0 Journal Article
%A Hao, Yunge
%A Tourlakis, George
%T An Arithmetically Complete Predicate Modal Logic
%J Bulletin of the Section of Logic
%D 2021
%P 513-541
%V 50
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2021_50_4_a3/
%G en
%F BSL_2021_50_4_a3
Hao, Yunge; Tourlakis, George. An Arithmetically Complete Predicate Modal Logic. Bulletin of the Section of Logic, Tome 50 (2021) no. 4, pp. 513-541. http://geodesic.mathdoc.fr/item/BSL_2021_50_4_a3/

[1] S. Artemov, G. Dzhaparidze, Finite Kripke Models and Predicate Logics of Provability, Journal of Symbolic Logic, vol. 55(3) (1990), pp. 1090–1098 | DOI

[2] A. Avron, On modal systems having arithmetical interpretations, Journal of Symbolic Logic, vol. 49(3) (1984), pp. 935–942 | DOI

[3] G. Boolos, The logic of provability, Cambridge University Press (2003) | DOI

[4] E. W. Dijkstra, C. S. Scholten, Predicate Calculus and Program Semantics, Springer, New York (1990) | DOI

[5] K. Fine, Failures of the interpolation lemma in quantfied modal logic, Journal of Symbolic Logic, vol. 44(2) (1979), pp. 201–206 | DOI

[6] 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

[7] K. Gödel, Eine Interpretation des intuitionistischen Aussagenkalkuls, Ergebnisse Math, vol. 4 (1933), pp. 39–40.

[8] D. Gries, F. B. Schneider, A Logical Approach to Discrete Math, Springer, New York (1994) | DOI

[9] 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

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

[11] D. Hilbert, P. Bernays, Grundlagen der Mathematik I and II, Springer, New York (1968) | DOI

[12] 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

[13] F. Kibedi, G. Tourlakis, A Modal Extension of Weak Generalisation Predicate Logic, Logic Journal of IGPL, vol. 14(4) (2006), pp. 591–621 | DOI

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

[15] S. A. Kripke, A completeness theorem in modal logic, Journal of Symbolic Logic, vol. 24(1) (1959), pp. 1–14 | DOI

[16] E. Mendelson, Introduction to Mathematical Logic, 3rd ed., Wadsworth Brooks, Monterey, CA (1987) | DOI

[17] F. Montagna, The predicate modal logic of provability, Notre Dame Journal of Formal Logic, vol. 25(2) (1984), pp. 179–189 | DOI

[18] 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

[19] 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

[20] 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.

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

[22] C. Smorynski, Self-Reference and Modal Logic, Springer, New York (1985) | DOI

[23] R. M. Solovay, Provability interpretations of modal logic, Israel Journal of Mathematics, vol. 25(3–4) (1976), pp. 287–304 | DOI

[24] G. Tourlakis, Lectures in Logic and Set Theory, Volume 1: Mathematical Logic, Cambridge University Press, Cambridge (2003) | DOI

[25] G. Tourlakis, Mathematical Logic, John Wiley Sons, Hoboken, NJ (2008) | DOI

[26] 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

[27] 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.

[28] 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.

[29] 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

[30] R. E. Yavorsky, On Arithmetical Completeness of First-Order Logics of Provability, Advances in Modal Logic, (2002), pp. 1–16 | DOI