Geodesic
A simplified proof of arithmetical completeness theorem for provability logic $\mathbf{GLP}$
Informatics and Automation, Algorithmic aspects of algebra and logic, Tome 274 (2011), pp. 32-40 
L. D. Beklemishev. A simplified proof of arithmetical completeness theorem for provability logic $\mathbf{GLP}$. Informatics and Automation, Algorithmic aspects of algebra and logic, Tome 274 (2011), pp. 32-40. http://geodesic.mathdoc.fr/item/TRSPY_2011_274_a3/
@article{TRSPY_2011_274_a3,
     author = {L. D. Beklemishev},
     title = {A simplified proof of arithmetical completeness theorem for provability logic $\mathbf{GLP}$},
     journal = {Informatics and Automation},
     pages = {32--40},
     year = {2011},
     volume = {274},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/TRSPY_2011_274_a3/}
}
TY  - JOUR
AU  - L. D. Beklemishev
TI  - A simplified proof of arithmetical completeness theorem for provability logic $\mathbf{GLP}$
JO  - Informatics and Automation
PY  - 2011
SP  - 32
EP  - 40
VL  - 274
UR  - http://geodesic.mathdoc.fr/item/TRSPY_2011_274_a3/
LA  - ru
ID  - TRSPY_2011_274_a3
ER  - 
%0 Journal Article
%A L. D. Beklemishev
%T A simplified proof of arithmetical completeness theorem for provability logic $\mathbf{GLP}$
%J Informatics and Automation
%D 2011
%P 32-40
%V 274
%U http://geodesic.mathdoc.fr/item/TRSPY_2011_274_a3/
%G ru
%F TRSPY_2011_274_a3

Voir la notice de l'article provenant de la source Math-Net.Ru

We present a simplified proof of Japaridze's arithmetical completeness theorem for the well-known polymodal provability logic $\mathbf{GLP}$. The simplification is achieved by employing a fragment $\mathbf J$ of $\mathbf{GLP}$ that enjoys a more convenient Kripke-style semantics than the logic considered in the papers by Ignatiev and Boolos. In particular, this allows us to simplify the arithmetical fixed point construction and to bring it closer to the standard construction due to Solovay.

[1] Beklemishev L.D., “Skhemy refleksii i algebry dokazuemosti v formalnoi arifmetike”, UMN, 60:2 (2005), 3–78 | DOI | MR | Zbl

[2] Beklemishev L.D., “Kripke semantics for provability logic GLP”, Ann. Pure and Appl. Logic, 161 (2010), 756–774 ; Logic Group Preprint Ser., 260, Univ. Utrecht, Oct. 2007 http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint260.pdf | DOI | MR | Zbl

[3] Boolos G., The logic of provability, Cambridge Univ. Press, Cambridge, 1993 | MR | Zbl

[4] Ignatiev K.N., “On strong provability predicates and the associated modal logics”, J. Symb. Log., 58 (1993), 249–290 | DOI | MR | Zbl

[5] Dzhaparidze G.K., Modalno-logicheskie sredstva issledovaniya dokazuemosti, Dis. ... kand. filos. nauk, MGU, M., 1986.

[6] Smorinskii K., “Teoremy o nepolnote”, Spravochnaya kniga po matematicheskoi logike. Ch. 4: Teoriya dokazatelstv i konstruktivnaya matematika, Pod red. Dzh. Barvaisa, Nauka, M., 1983, 9–53

[7] Solovay R.M., “Provability interpretations of modal logic”, Isr. J. Math., 25 (1976), 287–304 | DOI | MR | Zbl