Uniform interpolation and the existence of sequent calculi

DOI10.1016/J.APAL.2019.05.008MaRDI QIDQ2326416zbMATH OpenOpenAlexWikidataFDO

Publication date 7 October 2019

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://dspace.library.uu.nl/handle/1874/394381

intermediate logic intuitionistic modal logic propositional quantifiers sequent calculus uniform interpolation

Subsystems of classical logic (including intuitionistic logic) (03B20) Modal logic (including the logic of norms) (03B45) Intermediate logics (03B55) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Review text

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).

Recommendations

Cites work

Cited in

(24)

This page was built for publication: Uniform interpolation and the existence of sequent calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2326416)