One of the advantages of using sequent systems as a framework for logical reasoning is that the resulting calculi are often simple, have good proof theoretical properties (like cut-elimination, consistency, etc) and can be easily implemented, eg using rewriting.

Hence it would be heaven if we could add axioms in mathematical theories to first order logics and reason about them using all the machinery already built for the sequent framework. Indeed, the general problem of extending standard proof-theoretical results obtained for pure logic to certain classes of non-logical axioms has been the focus of attention for quite some time now.

The main obstacle for this agenda is that adding non-logical axioms to systems while still maintaining the good proof theoretical properties is not an easy task. In fact, adding naively axioms to sequent systems often result in non cut-free systems. One way of circumventing this problem is by treating axioms as theories, added to the sequent context. This is already in Gentzen’s consistency proof of elementary arithmetic. Now the derivations have only logical axioms as premises, and cut elimination applies.

But we can do better by transforming axioms into inference rules. In this talk, we will propose a systematic way of adding inference rules to sequent systems. The proposal will be based on the notions of focusing and polarities. We will also discuss how our framework escalates to hypersequents and systems of rules, and the application of this to modal logics, proofs explanation and SMT solvers.

This is a joint work with Dale Miller, Sonia Marin, Marco Volpe, Francesca Poggiolesi and Yoni Zohar.