ИСТИНА

The provability logic GLP introduced by G. Japaridze is a propositional polymodal logic with important applications in proof theory, specificially, in ordinal analysis of arithmetic. Though being incomplete with respect to any class of Kripke frames, the logic GLP is complete for its neighbourhood interpretation. This completeness result, established by L. Beklemishev and D. Gabelaia, implies strong neighbourhood completeness of this system for the case of the so-called local semantic consequence relation. In this article, we consider Hilbert-style non-well-founded derivations in the provability logic GLP and establish that GLP with the obtained derivability relation is strongly neighbourhood complete in the case of the global semantic consequence relation.