Bounded Proofs and Step Frames

The longstanding research line investigating free algebra constructions in modal logic from an algebraic and coalgebraic point of view recently lead to the notion of a one-step frame [14], [8]. A one-step frame is a two-sorted structure which admits interpretations of modal formulae without nested modal operators. In this paper, we exploit the potential of one-step frames for investigating proof-theoretic aspects. This includes developing a method which detects when a specific rule-based calculus Ax axiomatizing a given logic

L

has the so-called bounded proof property. This property is a kind of an analytic subformula property limiting the proof search space. We define conservative one-step frames and prove that every finite conservative one-step frame for Ax is a p-morphic image of a finite Kripke frame for

L

iff Ax has the bounded proof property and

L

has the finite model property. This result, combined with a ‘one-step version’ of the classical correspondence theory, turns out to be quite powerful in applications. For simple logics such as

K

,

T

,

K4

,

S4

, etc, establishing basic metatheoretical properties becomes a completely automatic task (the related proof obligations can be instantaneously discharged by current first-order provers). For more complicated logics, some ingenuity is needed, however we successfully applied our uniform method to Avron’s cut-free system for

GL

and to Goré’s cut-free system for

S4.3

.