Paper detail

Positive provability logic for uniform reflection principles

We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant `true&#39; by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ωcorresponds to the full uniform reflection schema, whereas n<ωcorresponds to its restriction to arithmetical Π_{n+1}-formulas. This calculus is shown to be complete w.r.t. a suitable class of finite Kripke models and to be decidable in polynomial time.