zbMATH — the first resource for mathematics

On the reflection calculus with partial conservativity operators. (English) Zbl 06820460
Kennedy, Juliette (ed.) et al., Logic, language, information, and computation. 24th international workshop, WoLLIC 2017, London, UK, July 18–21, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10388, 48-67 (2017).
Summary: 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 the constant “true” using only conjunction and the diamond modalities which are interpreted in Peano arithmetic as restricted uniform reflection principles.{
}We extend the language of \(\mathrm {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 \(\varPi ^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 \(\mathrm {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 \(<\varepsilon _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.
For the entire collection see [Zbl 1369.03021].

03B70 Logic in computer science
Full Text: DOI