We provide a syntactical translation from poly-modal provability logic \(GLP\) to the Gödel-Löb logic \(GL\). This translation has two parts: first we use a translation similar to the Beklemishev’s translation [1] from \(GLP\) to a subsytem \(J^-\) of \(GLP\), in which the monotonicity axiom \([n] A\to[n+1] A\) is replaced by \([n] A\to [n+i] [n] A\). Then we define a translation which makes nested boxes ascending, i.e. if \([n]\) occurs inside some \([m]\), then \(n\geq m\).

Finally we provide a simple Kripke-style semantics for \(J^-\) which enables us to reprove arithmetical completeness of \(GLP\).

Bibliography

1. L. D. Beklemishev,Kripke semantics for provability logic GLP, Annals of Pure and Applied Logic 161 (2010) 756–774.