Provability logic—a short introduction (Q4378052)

Provability logic is a simple modal description of the famous Gödel predicate Bew. In the paper, the author gives a self-contained description of provability logic. More extensive and detailed introductions to provability logic are given by \textit{G. Boolos} [The unprovability of consistency (1979; Zbl 0409.03009)], \textit{C. Smorynski} [Self-reference and modal logic (1985; Zbl 0596.03001)], and \textit{G. Boolos} [The logic of provability (1993; Zbl 0891.03004)]. Some of the results presented in the paper do not appear in these books. The paper is divided into fourteen chapters, the eight first ones presenting Solovay's completeness theorems. The main themes of the first four chapters are: Bernays-Löb conditions, arithmetical interpretation, arithmetically valid and \(\omega\)-valid formulas, classical modal logic, Kripke models, local reflection principle and the like. In the fifth chapter, the author gives a simple new proof of the fixed-point theorem for the system GL (Gödel-Löb). In the sixth chapter the proof of Solovay's completeness theorems are given. In the seventh and eighth chapter, the author presents some examples of applications of the former results (Rosser's theorem and Goldfarb's principle; modal rule of inference). The ninth, tenth, eleventh, and twelfth chapter include some bimodal logics (for example interpretability logic IL). Chapter 13 concerns quantified provability logic. The last chapter is devoted to some related topics, for example interpolation lemma, Beth's definability theorem, classification theorem of Beklamishev. Most of the results in the chapters 9-14 are given without proof.