Positive provability logic for uniform reflection principles.

*(English)*Zbl 1322.03041Since 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, 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.

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, 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.

Reviewer: Osamu Sonobe (Follonica)

##### MSC:

03F45 | Provability logics and related algebras (e.g., diagonalizable algebras) |

03B45 | Modal logic (including the logic of norms) |

03F30 | First-order arithmetic and fragments |

##### Citations:

Zbl 1315.03113
PDF
BibTeX
XML
Cite

\textit{L. Beklemishev}, Ann. Pure Appl. Logic 165, No. 1, 82--105 (2014; Zbl 1322.03041)

**OpenURL**

##### References:

[1] | Beklemishev, L. D., Provability algebras and proof-theoretic ordinals, I, Ann. Pure Appl. Logic, 128, 103-123, (2004) · Zbl 1048.03045 |

[2] | Beklemishev, L. D., Reflection principles and provability algebras in formal arithmetic, Uspekhi Mat. Nauk, Russian Math. Surveys, 60, 2, 197-268, (2005), (in Russian); English translation · Zbl 1097.03054 |

[3] | Beklemishev, L. D., Kripke semantics for provability logic GLP, Ann. Pure Appl. Logic, 161, 756-774, (2010) · Zbl 1223.03046 |

[4] | Beklemishev, L. D., A simplified proof of the arithmetical completeness theorem for the provability logic GLP, Tr. Mat. Inst. Steklova, Proc. Steklov Inst. Math., 274, 3, 25-33, (2011), English translation · Zbl 1294.03038 |

[5] | Beklemishev, L. D., Calibrating provability logic: from modal logic to reflection calculus, (Bolander, T.; Braüner, T.; Ghilardi, S.; Moss, L., Adv. Modal Log., vol. 9, (2012), College Publications London), 89-94 · Zbl 1331.03040 |

[6] | Beklemishev, L.; Gabelaia, D., Topological completeness of the provability logic GLP, Ann. Pure Appl. Logic, 164, 12, 1201-1223, (2013) · Zbl 1320.03088 |

[7] | Beklemishev, L.; Fernández-Duque, D.; Joosten, J., On provability logics with linearly ordered modalities, (October 2012), preprint |

[8] | Boolos, G., The logic of provability, (1993), Cambridge University Press Cambridge · Zbl 0891.03004 |

[9] | Cook, S. A.; Rekhow, R. A., Time bounded random access machines, J. Comput. System Sci., 7, 354-374, (1977) |

[10] | Dashkov, E. V., On the positive fragment of the polymodal provability logic GLP, Mat. Zametki, Math. Notes, 91, 3, 318-333, (2012), English translation · Zbl 1315.03113 |

[11] | Feferman, S., Arithmetization of metamathematics in a general setting, Fund. Math., 49, 35-92, (1960) · Zbl 0095.24301 |

[12] | Fernández-Duque, D.; Joosten, J., The omega-rule interpretation of transfinite provability logic, (February 2013), preprint |

[13] | Hájek, P.; Pudlák, P., Metamathematics of first order arithmetic, (1993), Springer-Verlag Berlin, Heidelberg, New York · Zbl 0781.03047 |

[14] | Halpern, J. Y.; Moses, Y., A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence, 54, 311-379, (1992) · Zbl 0762.68029 |

[15] | Ignatiev, K. N., On strong provability predicates and the associated modal logics, J. Symbolic Logic, 58, 249-290, (1993) · Zbl 0795.03082 |

[16] | Japaridze, G. K., The modal logical means of investigation of provability, (1986), (in Russian) |

[17] | Kreisel, G.; Lévy, A., Reflection principles and their use for establishing the complexity of axiomatic systems, Z. Math. Log. Grundl. Math., 14, 97-142, (1968) · Zbl 0167.01302 |

[18] | Smoryński, C., The incompleteness theorems, (Barwise, J., Handbook of Mathematical Logic, (1977), North-Holland Amsterdam), 821-865 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.