Raheleh Jalali
Institute of Mathematics of the Czech Academy of Sciences

In [2], Iemhoff introduced a syntactic generic form for a certain class of sequent-style rules that she called focused rules. Intuitively speaking, these rules are the rules in which only one side of the sequents is active and the consequence inherits the atomic formulas of the premises. This introduction then led to the implication that the existence of a terminating sequent calculus consisting of these focused rules and the usual \(\mathbf{LJ}\) axioms implies the uniform interpolation property of the super-intuitionistic logic that the calculus captures. In this talk, we will strengthen this implication in two different directions. First, we lower down the base logic from intuitionistic logic to \(\mathbf{FL_e}\) to also cover the whole world of sub-structural logics and secondly we will generalize the syntactic form of the rules to a more general form in which both sides of the rule are allowed to be active. The resulting implication then has two major applications. In its positive side, it provides a uniform method to establish uniform interpolation property for logics \(\mathbf{FL_e}\), \(\mathbf{FL_{ew}}\), \(\mathbf{CFL_e}\), \(\mathbf{CFL_{ew}}\), \(\mathbf{IPC}\), \(\mathbf{CPC}\), their \(\mathbf{K}\) and \(\mathbf{KD}\)-type modal extensions and some basic non-normal modal logics including \(\mathbf{E}\), \(\mathbf{M}\), \(\mathbf{MC}\) and \(\mathbf{MN}\). On its negative side though, the connection implies that no extension of \(\mathbf{FL_e}\) enjoys a certain natural type of terminating sequent calculus unless it has the uniform interpolation property. This negative reading of the result then leads to the exclusion of almost all super-intutionistic logics (except seven of them), the logic \(\mathbf{K4}\) and almost all the extensions of the logic \(\mathbf{S4}\) (except six of them) from having such a reasonable calculus.

This presentation is based on joint work with Amir Akbar Tabatabai [1]

[1] Akbar Tabatabai, Amir, and Raheleh Jalali. Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation. Manuscript (2019) https://arxiv.org/abs/1808.06258

[2] Iemhoff, Rosalie. Uniform interpolation and the existence of sequent calculi. Annals of Pure and Applied Logic (2019).