The bounded proof property via step algebras and step frames

Abstract

We develop a semantic criterion for a specific rule-based calculus Ax axiomatizing a given logic L to have the so-called bounded proof property. This property is a kind of an analytic subformula property limiting the proof search space. Our main tools are one-step frames and one-step algebras. These structures were used in [23], [11] to construct free algebras of modal logics via coalgebraic methods. In this paper, we use one-step algebras and one-step frames to investigating proof-theoretic aspects of modal logics.

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 the- ory, turns out to be quite powerful in case studies. 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 still needed, however we were able to successfully apply our uni- form method to Avron’s cut-free system for GL, to Gor ́e’s cut-free system for S4.3, and to Ohnishi-Matsumoto’s analytic system for S5.

This paper is a slightly extended version of the technical report published in April 2013. The only changes are: a new title and new Sections 1.2 and 9.3.