Positive provability logic for uniform reflection principles (Q392274)

Since the arithmetical provability interpretation of modality was established by Solovay about 40 years ago, the study of provability modal logic GL has been developing under various perspectives. Japaridze introduced a polymodal extension GLP of GL with modalities labeled by natural numbers for a finer analysis of provability in relation to the recursive hierarchy. Dashkov and the author of this paper study recently the strictly positive fragment of GLP as reflection calculus RC, where a (GLP-)formula is called strictly positive if it is built up on propositional variables and truth constant by conjunction and diamonds only, and the strictly positive fragment means the fragment constituted by implications of strictly positive formulas. Restricting the language thus, we are allowed to employ provability interpretations of modality more flexibly. In fact, propositional variables can be interpreted as arithmetical theories rather than individual sentences on the base of truth constant for PA, conjunction for the union of theories, the diamond labeled by \(n\) for the \(n\)-consistency of theory, and the (outer-most) implication for reverse (set-)inclusion of theories. It is important that such an interpretation is not extendable to the full modal language since the negation of a theory would not be well-defined. This approach also leads naturally to another modality (labeled by \(\omega\)) for the full uniform reflection schema, so that RC can be extended to RC\(\omega\) with a characteristic axiom for the newly introduced \(\omega\)-modality. The fragment enjoys, in addition, several nice characteristics as a system of modal logic. For instance, \textit{E. V. Dashkov} [Math. Notes 91, No. 3, 318--333 (2012; Zbl 1315.03113); translation from Mat. Zametki 3, 331--346 (2012)] has already shown that RC is Kripke complete with finite model property, which contrasts sharply with the Kripke incompleteness of GLP. In this paper, the completeness of RC\(\omega\) is established with respect to the above mentioned arithmetical interpretation as well as to a suitable class of finite Kripke models. Moreover, it is shown to be decidable in polynomial time. The author suggests also some approaches for further study of positive modal logic.