Исчисление для схем рефлексии и спектры консервативности

Успехи математических наук. 2018. Т. 74. № 4. С. 3–52.

Beklemishev L. D.

Strictly positive logics recently attracted attention both in the description logic and in the provability logic communities for their combination of efficiency and sufficient expressivity. The language of Reflection Calculus RC consists of implications between formulas built up from propositional variables and constant `true' using only conjunction and diamond modalities which are interpreted in Peano arithmetic as restricted uniform reflection principles.

We extend the language of $\Rc$ by another series of modalities representing the operators associating with a given arithmetical theory $T$ its fragment axiomatized by all theorems of $T$ of arithmetical complexity $\Pi^0_n$, for all $n>0$. We note that such operators, in a strong sense, cannot be represented in the full language of modal logic.

We formulate a formal system $\Rcn$ extending $\Rc$ that is sound and, as we conjecture, complete under this interpretation. We show that in this system one is able to express iterations of reflection principles up to any ordinal $<\ge_0$. Secondly, we provide normal forms for its variable-free fragment. Thereby, this fragment is shown to be algorithmically decidable and complete w.r.t. its natural arithmetical semantics.

In the last part of the paper we characterize in several natural ways the Lindenbaum--Tarski algebra of the variable-free fragment of $\Rcn$ and its dual Kripke structure. Most importantly, the elements of this algebra correspond to the sequences of proof-theoretic $\Pi^0_{n+1}$-ordinals of bounded fragments of Peano arithmetic called conservativity spectra, as well as to the points of the well-known Ignatiev Kripke model.

 

Keywords: модальная логика, Strictly positive logics, Reflection principle, Provability, GLP, схема рефлексии