Bounded proofs and step frames

The longstanding research line investigating free algebra con- structions 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 prop- erty. 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 pow- erful in applications. For simple logics such as K, T, K4, S4, etc, estab- lishing 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 ingenu- ity 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.