Display-Type Calculi and Their Cut Elimination Metatheorem

ABSTRACT. The range of non-classical logics has been rapidly expanding, driven by influences from other fields which have opened up new opportunities for applications. The logical formalisms which have been developed as a result of this interaction have attracted the interest of a wider research community than the logicians, and their theory has been intensively investigated, especially w.r.t.\ their semantics and computational complexity.

However, most of these logics lack a comparable proof-theoretic development. More often than not, the hurdles preventing a standard proof-theoretic development for these logics are due precisely to some of their defining features which make them suitable for applications, such as e.g.\ their not being closed under uniform substitution, or the fact that (the semantic interpretations of) key connectives are not adjoints.

These difficulties caused the existing proposals in literature to be often ad hoc, not easily generalisable, and more in general lacking a smooth proof-theoretic behaviour. In particular, the difficulty in smoothly transferring results from one logic to another is a problem in itself, since these logics typically come in large families (consider for instance the family of dynamic logics), and hence proof-theoretic approaches which uniformly apply to each logic in a given family are in high demand (for an expanded discussion of the existing proof systems for dynamic epistemic logics, see [5, section 3]).

The problem of the transfer of results, tools and methodologies has been addressed in the proof-theoretic literature for the families of substructural and modal logics, and has given rise to the development of several generalisations of Gentzen sequent calculi (such as hyper-, higher level-, display- or labelled-sequent calculi).

In this talk we focus on the core technical aspects of a proof-theoretic methodology and set-up closely linked to display logic [2] and basic logic [1]. Instances of this set-up have appeared in [5] and [6] to account for (nonclassical versions of) Baltag-Moss-Solecki's dynamic epistemic logic. In ongoing work, this set-up is being applied to propositional dynamic logic [3], monotone modal logic [4], game logic, and linear logic.

The present set-up, which we refer to as \textit{display-type calculi}, generalizes display calculi in two aspects: by allowing multi-type languages, and by dropping the full display property. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g.\ for a smooth proof-theoretic treatment of multi-modal and dynamic logics [6, 3]. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals [4].

One technical aspect which guarantees the cut elimination meta-theorem to go through for display-type calculi, even in the absence of the full display property, concerns the strengthening of the \textit{separation} property (requiring principal formulas in introduction rules to appear in isolation) to the \textit{visibility} property. Visibility requires \textit{all active formulas} in introduction rules to occur in isolation. This property was recognized to be crucial for the cut elimination theorem of basic logic [1].

However, in the present set-up of display-type calculi, visibility is also weakened, in the sense that, in order to account for logics that are not closed under uniform substitution [5, 6], principal formulas in axioms are not required to occur in isolation.

In the proposed talk, we will illustrate the basic principles of the multi-type environment, and also how the above combination of weakenings, strengthenings of the separation property concurs to guaranteeing the cut elimination meta-theorem for display-type calculi.

Time permitting, we will also discuss some difficulties that still arise in the case of PDL and some ideas towards treating predicative logics.

\bigskip {\noindent\large\textbf{References}} \smallskip

{\small \noindent [1] G.~Battilotti, C.~Faggian, G.~Sambin, \emph{Basic logic: Reflection, Symmetry, Visibility}, Journal of Symbolic Logic 65 (2000).

\noindent [2] N.~Belnap, \emph{Display logic}, J. of Philosophical Logic 11 (1982), pp.~375-417.

\noindent [3] S.~Frittella, A.~Kurz, A.~Palmigiano, \emph{Multi-type Display Calculus for Propositional Dynamic Logic}, submitted to JLC - Special Issue on Substructural Logic and Information Dynamics (2014).

\noindent [4] S.~Frittella, G.~Greco, \emph{Display-type Sequent Calculus For Monotone Modal Logic}, submitted to Advances in Modal Logic (2014).

\noindent [5] S.~Frittella, G.~Greco, A.~Kurz, A.~Palmigiano, and V.~Sikimi\'{c}, \emph{A Proof-theoretic Semantic Analysis Of Dynamic Epistemic Logic}, to appear in JLC - Special Issue on Substructural Logic and Information Dynamics (2014).

\noindent [6] S.~Frittella, G.~Greco, A.~Kurz, A.~Palmigiano, and V.~Sikimi\'{c}, \emph{Multi-type Display Calculus For Dynamic Epistemic Logic}, to appear in JLC - Special Issue on Substructural Logic and Information Dynamics (2014).