Reflection Calculus with Conservativity Modalities
Lev Beklemishev
We consider positive provability logic RC enriched by a series of operations associating with an arithmetical theory the set of all its theorems of arithmetical complexity Π0n+1 (for all natural numbers n). We discuss the expressive power of this logic and a normal form theorem for its closed fragment, which is related to the notion of Π0n+1-ordinal of a formal theory.