?
On the Reflection Calculus with Partial Conservativity Operators
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 RC
We formulate a formal system extending RC