Positive provability logic for uniform reflection principles

TL;DR

This paper introduces a modal logic framework for uniform reflection principles in arithmetic, providing a complete, decidable calculus with modalities representing different reflection strengths.

Contribution

It formulates an arithmetically complete and polynomial-time decidable calculus for uniform reflection principles using a simplified modal language.

Findings

Complete calculus with natural number and omega modalities

Kripke model semantics for the logic

Decidability in polynomial time

Abstract

We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant `true' 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 \omega, where \omega corresponds to the full uniform reflection schema, whereas n<\omega corresponds to its restriction to arithmetical \Pi_{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.