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.
1. Boolos, George (1993), The Logic of Provability, London and New York: Cambridge university press.
2. de Jongh, D.H.J.; Montagna, F. (1988), “Provable Fixed Points”, Mathematical Logic Quarterly, 34(3): 229–250.
3. Gödel, K., (1933), “Eine Interpretation des intuitionistischen Aussagenkalküls,” Ergebnisse eines Mathematischen Kolloquiums, 4: 39–40; translation “An Interpretation of the Intuitionistic Propositional Calculus,” in K. Gödel, Collected Works, S. Feferman et al. (eds.), Oxford and New York: Oxford University Press, Volume 1, 1986, pp. 300–302.
4. Grzegorczyk, Andrzej (1967), “Some relational systems and the associated topological spaces”, Fundamenta Mathematicae, Volume 60, pp. 223–231
5. Henkin, L., 1952, “A Problem Concerning Provability,” Journal of Symbolic Logic, 17: 160.
6. Hughes, G.E.; Cresswell, M.J. (1996), A New Introduction to Modal Logic, London and New York: Routledge.
7. Kushida, H. (2010), “The Modal Logic of Gödel Sentences”, Journal of Philosophical Logic, Vol.39, p.577–590.
8. Kushida, H. (2019), “A Proof Theory for the Logic of Provability in True Arithmetic”, studia Logica, Vol. 108, p. 857–875.
9. Löb, M.H. (1955), “Solution of a Problem of Leon Henkin,” Journal of Symbolic Logic, 20: 115–118.
10. McKinsey, J. C. C.; Tarski, Alfred (1984), “Some Theorems About the Sentential Calculi of Lewis and Heyting”, The Journal of Symbolic Logic, Vol. 13, No. 1, pp. 1-15.
11. Movahed, Zia (2006), Modal Logic, Tehran: Hermes press.
12. Nabavi, L. (2003), An Introduction to Modal Logic (1th ed.), Teharn: TMU.
13. Negri, S. (2005), “Proof Analysis in Modal Logic,” Journal of Philosophical Logic, 50: 507–544.
14. Negri, S., (2014), “Proofs and Countermodels in Non-classical Logics,” Logica Universalis, 8(1): 25–60.
15. Sambin, G. (1976), “An Effective Fixed Point Theorem in Intuitionistic Diagonalizable Algebras (The Algebraization of the Theories Which Express Theor, IX),” Studia Logica 35: 345–361.
16. Sambin, G., Valentini, S. (1982), “The Modal Logic of Provability. The Sequential Approach,” Journal of Philosophical Logic, 11(3): 311–342.
17. Segerberg, Krister (1971), “An Essay in Classical Modal Logic”, PhD Thesis, Stanford University.
18. SEP (2017), “Provability Logic”, First published Wed Apr 2, 2003; substantive revision Wed Apr 5, 2017:
19. Solovay, R.M. (1976), “Provability interpretations of modal logic”. Israel J. Math. 25, 287–304.