Dzhaparidze, G. K. Provability logic with modalities for arithmetical complexities. (English) Zbl 0714.03018 Soobshch. Akad. Nauk Gruz. SSR 138, No. 3, 481-484 (1990). The propositional system HGL with modalities \(\square\) (for provability in classical arithmetic), \(\Sigma_ i\), \(\Sigma^+_ i\) (for the property of being provably equivalent to a \(\Sigma^ o_ i\) formula, resp. to a Boolean combination of such formulas) is axiomatized by the standard axioms for provability logic, closure property of \(\Sigma_ i\), \(\Sigma^+_ i\) with respect to \(\wedge\), \(\vee\), \(\neg\), implications \(\Sigma\) \(A\vee \square (A\to B)\to \Sigma B\), \(\Sigma\) \(A\to \square \Sigma A\), \(\Sigma A\to \Sigma 'A\) for suitable \(\Sigma\), \(\Sigma '\), and \(\Sigma\perp\), \(\Sigma\square A\), \(\Sigma_ 1A\to \square (A\to \square A)\), \(\Sigma \Sigma 'A\) for all \(\Sigma\), \(\Sigma '\) among \(\Sigma_ i\), \(\Sigma^+_ i\). The proof uses Kripke-type semantics with separate accessibility relations for different modalities. Reviewer: G.Mints Cited in 4 Documents MSC: 03B45 Modal logic (including the logic of norms) 03F30 First-order arithmetic and fragments 03F40 Gödel numberings and issues of incompleteness Keywords:HGL; provability in classical arithmetic; provability logic; Kripke-type semantics PDFBibTeX XMLCite \textit{G. K. Dzhaparidze}, Soobshch. Akad. Nauk Gruz. SSR 138, No. 3, 481--484 (1990; Zbl 0714.03018)