Comparing Sequent Calculi via Hilbert-Style Axioms

ABSTRACT. In this talk I will consider the question of how to compare and evaluate the expressive strength of different formats of Gentzen-style systems. More precisely, the general question is which logics can be captured in the different frameworks. Of course some results are clear: e.g. since every standard sequent can be seen as a hypersequent with only one component or as a nested sequent without the nesting, every logic which can be captured in the framework of standard sequent calculus can be captured in the framework of hypersequent or nested sequent calculi as well. Other results are given by explicitly translating one framework into another, see e.g. [Gore and Ramanayake:2012].

While such results certainly establish important connections between the different frameworks, they only provide information on the expressive strength of one Gentzen-style framework relative to another one. Yet we are also interested in the absolute expressive strength and in particular the limits of what can be expressed in the different frameworks in a meaningful way. The qualification "in a meaningful way'' here is important, since of course given any set A of formulae the sequent calculus with groundsequents =>a for every a in A will serve to derive exactly the formulae in A, even in a cut-free way. Thus to make this question non-trivial we also need to restrict the format of the rules in the different frameworks.

Comparing the different frameworks and formats of rules finally can be done by identifying characterisations for them in a single common framework. Since we would like to compare extensions of sequent calculus, this should be a framework outside the class of Gentzen-style frameworks, and ideally the characterisations should provide a way of quickly determining which Gentzen-style framework is suitable for a particular logic. For this purpose here we choose the framework of Hilbert-style axiom systems. This gives a high degree of flexibility and allows in particular to capture non-normal modal logics and logics based on other than classical propositional logic. A characterisation of a specific Gentzen-style framework together with a specific format of rules then is given by an ideally purely syntactically defined class of axioms together with translations from rules of the considered format and framework into axioms of this class and vice versa. The prime example for this method is Kracht's result characterising those modal temporal logics which can be captured by structural rules in a display calculus satisfying Belnap's conditions for cut elimination as exactly the logics axiomatisable by primitive axioms [Kracht:1996]. Another example is the characterisation of structural rules in a sequent or hypersequent calculus for substructural logics by certain levels of the substructural hierarchy from [Ciabattoni et al:2008]. Apart from providing a first step for the construction of analytic calculi from Hilbert axioms, this method also yields a way to show limitative results: By showing that a certain logic cannot be axiomatised by axioms of a specific (syntactically given) form we can show that the logic cannot be captured by the framework and format of rules corresponding to this class of axioms.

In this talk I will discuss some recent results in this spirit concerning logical rules of different formats in the frameworks of standard sequent calculi and hypersequent calculi. The logics under consideration are propositional modal logics such as Goedel Loeb logic GL or the logic of 2-transitive Kripke frames, and more generally, extensions of classical or intuitionistic propositional logic with additional not necessarily unary connectives.