Reflection calculus and conservativity spectra

L. D. Beklemishev

Trudy Matematicheskogo Instituta imeni V.A. Steklova, Tome 73 (2018) no. 4, pp. 569-613

Résumé

Strictly positive logics have 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, $\mathrm{RC}$, consists of implications between formulas built up from propositional variables and the constant ‘true’ using only conjunction and diamond modalities which are interpreted in Peano arithmetic as restricted uniform reflection principles. The language of $\mathrm{RC}$ is extended 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$. It is noted that such operators, in a strong sense, cannot be represented in the full language of modal logic. A formal system $\mathrm{RC}^\nabla$ is formulated that extends $\mathrm{RC}$ and is sound and (it is conjectured) complete under this interpretation. It is shown that in this system one is able to express the iterations of reflection principles up to any ordinal $\varepsilon_0$. Second, normal forms are provided for its variable-free fragment. This fragment is thereby shown to be algorithmically decidable and complete with respect to its natural arithmetical semantics. In the last part of the paper the Lindenbaum–Tarski algebra of the variable-free fragment of $\mathrm{RC}^\nabla$ and its dual Kripke structure are characterized in several natural ways. Most importantly, 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 points of Ignatiev's well-known Kripke model. Bibliography: 46 titles.

Détail

Keywords: strictly positive modal logic, reflection principle, conservativity, ordinal.
Mots-clés : RC