ИСТИНА

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 Π0 n , for all n > 0. We note that such operators, in a precise sense, cannot be represented in the full language of modal logic. We formulate a formal system 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 < ε0. On the other hand, we provide normal forms for its variable-free fragment. Thereby, the variable-free fragment is shown to be algorithmically decidable and complete w.r.t. its natural arithmetical semantics. The normal forms for the variable-free formulas of RC∇ are related in a canonical way to the collections of proof-theoretic ordinals of arithmetical theories for each complexity level Π0 n+1 that we call conservativity spectra. Joost Joosten [2] established a one-to-one correspondence between conservativity spectra (for a certain class of theories) and the points of the universal model for the variable-free fragment of GLP due to Konstantin Ignatiev [1]. The third part of our paper provides an algebraic model I for the variable-free fragment of RC∇. Our main theorem states the isomorphism of several representations of I: the Lindenbaum–Tarski algebra of the variable-free fragment of RC∇; a constructive representation in terms of sequences of ordinals below ε0; a representation in terms of the semilattice of bounded RC-theories and as the algebra of cones of the Ignatiev model.