An Arithmetically Complete Predicate Modal Logic

• Autorzy: Yunge Hao , George Tourlakis

Abstrakty

EN

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.

Słowa kluczowe

EN

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

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2021
• Tom: 50
• Numer: 4
• Strony: 513-541

Daty

wydano

2021

Twórcy

autor

Yunge Hao

• York University, Department of Electrical Engineering and Computer Science

autor

George Tourlakis

• York University, Department of Electrical Engineering and Computer Science

Bibliografia

• 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
• 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
• G. Boolos, The logic of provability, Cambridge University Press (2003), 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
• 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
• 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
• K. Gödel, Eine Interpretation des intuitionistischen Aussagenkalkuls, Ergebnisse Math, vol. 4 (1933), pp. 39–40.
• 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
• 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
• 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
• 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
• 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
• 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
• E. Mendelson, Introduction to Mathematical Logic, 3rd ed., Wadsworth & Brooks, Monterey, CA (1987), 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
• 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
• 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
• 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
• 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
• G. Tourlakis, Lectures in Logic and Set Theory, Volume 1: Mathematical Logic, Cambridge University Press, Cambridge (2003), DOI: https://doi.org/10.1017/CBO9780511615559
• G. Tourlakis, Mathematical Logic, John Wiley & Sons, Hoboken, NJ (2008), 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
• 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

Identyfikatory

DOI

10.18778/0138-0680.2021.18

nonstd.3pn.id

2033850