Propositional Provability Logics

Nabavi, L.; Mirsanei, S.A.

doi:10.58209/jpt.1.4.313

Propositional Provability Logics

Document Type : Original Research

Authors

L. Nabavi

S.A. Mirsanei

Department of Philosophy, Faculty of Humanities, Tarbiat Modares University, Tehran, Iran

https://doi.org/10.58209/jpt.1.4.313

Abstract

Discovering the differences between the various systems of modal logics was one of the advantages of inventing Kripke semantics. One of the most obvious examples is interpreting the necessity of provability in provability logic. According to Boolos in The Logic of Provability, by discovering this logic, we can say that the understanding of new issues in the field of argument was opened. In this paper, with a formal approach and with a descriptive-analytical and comparative method, the axiomatic propositional systems of the GL, Grz, and H, and their possible world semantics based on Kripke semantics are studied, as well as the sequent calculus of GL (in Peano arithmetic) and GLS (in the standard model) were introduced. Finally, the meta-theorems of soundness, consistency, and completeness of the GL were interpreted and proved.

Keywords

Provability Logic

modal logic

Axiomatic System

Proof Theory

Possible World Semantics

Meta-Theorems

Subjects

Logic and Philosophy of Logic (Modern)

-Avron A (1984). On modal systems having arithmetical interpretations. Journal of Symbolic Logic. 49(3):935-942.
-Borga M (1983). On some proof theoretical properties of the modal logic GL. Studia Logica. 42:453-459.
- Boolos G (1993). The logic of provability. Cambridge: Cambridge University press.
-Brighton J (2016). Cut-elimination for GLS using the terminability of its regress process. Journal of Philosophical Logic. 45:147-153.
-Davis M (1958). Computability and Unsolvability. New York: Dover.
- de Jongh DHJ, Montagna F (1988). Provable fixed points. Mathematical Logic Quarterly. 34(3):229-250.
-de Jongh DHJ, Montagna F (1987). Generic generalized Rosser fixed points. Studia Logica: An International Journal for Symbolic Logic. 46(2):193-203.
-Gore R, Ramanayake R (2012). Valentini’s cut-elimination for provability logic resolved. The Review of Symbolic Logic. 5(2):212-238.
- Gödel K (1986). An Interpretation of the Intuitionistic Propositional Calculus. In: Feferman S, et al, editors. K. Gödel Collected Works. Volume 1. New York: Oxford University Press. pp. 300–302. [German]
- Grzegorczyk A (1967). Some relational systems and the associated topological spaces. Fundamenta Mathematicae. 60:223-231.
- Henkin L (1952). A problem concerning provability. Journal of Symbolic Logic. 17: 160.
-Hilbert D, Bernays P (1939). Grundlagen der mathematik II. Berlin: Julius Springer.
- Hughes GE, Cresswell MJ (1997). A new introduction to modal logic. London: Routledge.
-Hughes GE, Cresswell MJ (1984). A companion to modal logic. London: Methuen.
- Kushida H (2010). The modal logic of Gödel sentences. Journal of Philosophical Logic. 39:577- 590.
- Kushida H (2019). A proof theory for the logic of provability in true arithmetic. Studia Logica. 108: 857-875.
- Löb MH (1955). Solution of a problem of Leon Henkin. Journal of Symbolic Logic, 20:115-118.
- McKinsey JCC, Tarski A (1948). Some theorems about the sentential calculi of Lewis and Heyting. The Journal of Symbolic Logic. 13(1):1-15.
- Movahed Z (2006). Modal logic. Tehran: Hermes press.
- Nabavi L (2004). An introduction to modal logic. 1st edition. Tehran: TMU Press. [Persian]
- Negri S (2005). Proof analysis in modal logic. Journal of Philosophical Logic. 50:507-544.
- Negri S (2014). Proofs and countermodels in non-classical logics. Logica Universalis. 8(1):25- 60.
-Poggiolesi F (2009). A purely syntactic and cut-free sequent calculus for the modal logic of provability. Review of Symbolic Logic. 2(4):593-611.
- Sambin G (1976). An effective fixed point theorem in intuitionistic diagonalizable algebras. Studia Logica 35(4):345-361.
- Sambin G, Valentini S (1982). The modal logic of provability, the sequential approach. Journal of Philosophical Logic. 11(3):311-342.
-Sasaki K (2001). Löb’s axiom and cut-elimination theorem. Mathematical Sciences and Information Engineering: Journal of the Nanzan Academic Society. 1:91-98.
- Segerberg KK (1971). An essay in classical modal logic [dissertation]. Stanford: Stanford University.
- Solovay RM (1976). Provability interpretations of modal logic. Israel Journal of Mathematics. 25:287-304.
-Smiley TJ (1963). The logical basis of ethics. Acta Philosophica Fennica. 16:237-246.
-Smoryński C (1985). Self-reference and modal logic. Vrlag: Springer.
-Shamkanov D (2015). Nested sequents for provability logic GLP. Logic Journal of the IGPL. 23(5):789-815.
- Verbrugge R (2017). Provability logic. In: Zalta EN, editor. The Stanford Encyclopedia of Philosophy.
-Valentini S (1983). The modal logic of provability: cut-elimination. Journal of Philosophical Logic. 12:471-476.