Uniform interpolation and the existence of sequent calculi (Q2326416): Difference between revisions

A propositional logic \(L\) has \textit{uniform interpolation} if for every formula \(\phi\) and variable \(p\), there are formulas \(\forall p\,\phi\) and \(\exists p\,\phi\) not containing \(p\) such that \begin{align*} \vdash_L\psi\to\phi&\iff\vdash_L\psi\to\forall p\,\phi,\\ \vdash_L\phi\to\psi&\iff\vdash_L\exists p\,\phi\to\psi \end{align*} for all formulas \(\psi\) not containing \(p\). It is known that logics with Craig interpolation are few and far between (e.g., only \(7\) out of the \(2^\omega\) intermediate logics have interpolation, due to \textit{L. L. Maksimova} [Algebra Logika 16, 643--681 (1977; Zbl 0403.03047)]), and uniform interpolation is even more scarce (e.g., the well-known modal logics S4 and K4 have interpolation, but not uniform interpolation, due to \textit{S. Ghilardi} and \textit{M. Zawadowski} [Stud. Log. 55, No. 2, 259--271 (1995; Zbl 0831.03008)] and \textit{M. Bílková} [Stud. Log. 85, No. 1, 1--31 (2007; Zbl 1113.03017)]). In [Arch. Math. Logic 58, No. 1--2, 155--181 (2019; Zbl 07006132)], the author introduced a proof-theoretic method to show uniform interpolation for modal logics that enjoy sequent calculi with certain syntactic properties. Here, the method is extended to intermediate logics and intuitionistic modal logics. More specifically, in the case of intermediate logics, a notion of \textit{focused} sequent rules is defined in the paper, with the main result being that any logic that has a reductive cut-admissible calculus extending the Dyckhoff-Hudelmaier intuitionistic calculus by focused rules has uniform interpolation. (Here, reductivity is a certain condition ensuring that proof search terminates.) This reproves the result of \textit{A. M. Pitts} [J. Symb. Log. 57, No. 1, 33--52 (1992; Zbl 0763.03009)] that intuitionistic logic has uniform interpolation; however, as only a handful of intermediate logics have uniform interpolation, the main impact of the theorem is that no intermediate logics except possibly the Maksimicent seven may have a sequent calculus of the above-mentioned form. Similarly, in the case of intuitionistic modal logics (with \(\Box\) but no \(\Diamond\)), the author defines the notion of focused modal rules, and proves that any logic that has a balanced calculus extending a Dyckhoff-like calculus for (\(\Box\)-only) iK with focused and modal focused rules has uniform interpolation. In particular, the \(\Diamond\)-free fragments of the logics iK and iKD have uniform interpolation (which is a new result).