19

                 Cut Elimination
      and Second Order Quantifier Elimination
               (Abstract of Tutorial)

                          Alessandra Palmigiano
   with Giuseppe Greco, Minghui Ma, Apostolos Tzimoulis, Zhiguang Zhao

                    Delft University of Technology, Netherlands


Display calculi, pioneered by Belnap [1], are a proof-theoretic framework gener-
alizing Gentzen’s sequent calculi, which have succeeded in endowing a large class
of modal logics with cut-free sequent calculi in a uniform and modular way. The
robustness and modularity of display calculi are rooted in a general methodology
for proving cut-elimination, which identifies conditions on the design of sequent
calculi which guarantee the success of a certain uniform strategy for syntactic
cut elimination.
    Recently, systematic connections have been established between algorithmic
correspondence theory, well known from the area of modal logic, and the theory
of display calculi. These connections originate from some seminal observations
made by Kracht [5], in the context of his characterization of the modal axioms
which can be effectively transformed into ‘analytic’ structural rules of display
calculi. In this context, a rule is ‘analytic’ if adding it to a display calculus
preserves Belnap’s cut-elimination theorem.
    The present tutorial illustrates these connections. Specifically, after intro-
ducing (proper) display calculi and discussing the uniform strategy for their
cut elimination, I will discuss how the two main tools of unified correspondence
theory [3], [2] (namely, (a) the ALBA algorithm for second order quantifier elim-
ination, and (b) the syntactically defined class of inductive inequalities in each
logical/algebraic signature of normal distributive lattice expansions) can be used
to produce analytic calculi for a certain subclass of inductive formulas (the an-
alytic inductive inequalities), and to exhaustively characterize this subclass as
the class of the ‘properly displayable’ logics.
    Time permitting, I will also discuss how the methodology of multi-type calculi
[4] can be used to circumvent this exhaustive characterization, and export these
techniques also to non analytic logics.


References
1. N. Belnap. Display logic. Journal of Philosophical Logic, 11:375–417, 1982.
2. W. Conradie, S. Ghilardi, and A. Palmigiano. Unified correspondence. In A. Baltag
   and S. Smets, editors, Johan van Benthem on Logic and Information Dynamics, vol-
   ume 5 of Outstanding Contributions to Logic, pages 933–975. Springer International
   Publishing, 2014.

Copyright c 2017 by the paper’s authors
In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro-
ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics,
Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org.
                                                                                   20

3. W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for
   non-distributive logics. Submitted. ArXiv preprint 1603.08515.
4. S. Frittella, G. Greco, A. Kurz, A. Palmigiano, and V. Sikimić. Multi-type sequent
   calculi. In M. Z. A. Indrzejczak and J. Kaczmarek, editors, Proceedings of Trends
   in Logic XIII, pages 81–93. Lodz University Press, 2014.
5. M. Kracht. Power and weakness of the modal display calculus. In Proof theory of
   modal logic, volume 2 of Applied Logic Series, pages 93–121. Kluwer, 1996.