On the Construction of Analytic Sequent Calculi for Sub-Classical Logics

ABSTRACT. We study the question of when a given set of derivable rules in some basic analytic propositional sequent calculus forms itself an analytic calculus. First, a general syntactic criterion for analyticity in the family of pure sequent calculi is presented. Next, given a basic calculus admitting this criterion, we provide a method for constructing weaker pure calculi by collecting simple derivable rules of the basic calculus. The obtained calculi are analytic-by-construction. While the criterion and the method are completely syntactic, our proofs are semantic, based on the interpretation of sequent calculi using non-deterministic valuation functions. The proposed framework is useful for developing sequent calculi for sub-classical logics, that are obtained as sets of simple derivable rules of the usual sequent calculus for classical logic. This includes a wide variety of paraconsistent logics, as well as some extensions of Gurevich and Neeman's primal infon logic.