Lev D. Beklemishev

Steklov Mathematical Inistitute

We deal with the fragment of propositional modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. We call such fragments strictly positive. 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. Moreover, strictly positive logics allow for alternative interpretations that are quite natural from a proof-theoretic point of view.

We consider a 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 the corresponding  system of strictly positive provability logic and study its properties.

We show that in this system one is able to express iterations of reflection principles up to any ordinal \(<\epsilon_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. We also characterize its Lindenbaum--Tarski algebra and its dual Kripke structure. The elements of this algebra correspond to the sequences of proof-theoretic \(\Pi^0_{n+1}\)-ordinals of bounded fragments of Peano arithmetic called \emph{conservativity spectra}, as well as to the points of the well-known Ignatiev Kripke model.