×

Uniform interpolation and the existence of sequent calculi. (English) Zbl 1475.03078

A propositional logic \(L\) has 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 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 S. Ghilardi and M. Zawadowski [Stud. Log. 55, No. 2, 259–271 (1995; Zbl 0831.03008)] and 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 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 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).

MSC:

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

References:

[1] Alizadeh, M.; Derakhshan, F.; Ono, H., Uniform interpolation in substructural logics, Rev. Symb. Log., 7, 3, 455-483 (2014) · Zbl 1337.03033
[2] Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press
[3] Bellin, G.; de Paiva, V.; Ritter, E., Extended Curry-Howard correspondence for a basic constructive modal logic, (Araces, C.; de Rijke, M., Proceedings of Methods for Modalities 2 (2001))
[4] Bierman, G.; de Paiva, V., On an intuitionistic modal logic, Studia Logica, 65, 3, 383-416 (2000) · Zbl 0963.03033
[5] Bílková, M., Interpolation in Modal Logics (2006), Charles University: Charles University Prague, PhD-thesis
[6] Bílková, M., Uniform interpolation and propositional quantifiers in modal logics, Studia Logica, 85, 1, 259-271 (2007) · Zbl 1113.03017
[7] Božić, M.; Došen, K., Models for normal intuitionistic modal logics, Studia Logica, 43, 3, 217-245 (1984) · Zbl 0634.03014
[8] Dershowitz, N.; Manna, Z., Proving termination with multiset orderings, Commun. ACM, 22, 465-476 (1979) · Zbl 0431.68016
[9] Došen, K., Models for Stronger normal intuitionistic modal logics, Studia Logica, 44, 1, 39-70 (1985) · Zbl 0634.03015
[10] Dyckhoff, R., Contraction-free sequent calculi for intuitionistic logic, J. Symbolic Logic, 57, 3, 795-807 (1992) · Zbl 0761.03004
[11] Ghilardi, S.; Zawadowski, M., Undefinability of propositional quantifiers in the modal system \(S4\), Studia Logica, 55, 259-271 (1995) · Zbl 0831.03008
[12] Ghilardi, S.; Zawadowski, M., Sheaves Games, and Model Completions: A Categorical Approach to Nonclassical Propositional Logics, Trends in Logic (Book 14) (2002), Springer · Zbl 1036.03001
[13] S. van Gool, G. Metcalfe, C. Tsinakis, Uniform interpolation and compact congruences (2016), submitted, https://doi.org/10.1016/j.apal.2017.05.001; S. van Gool, G. Metcalfe, C. Tsinakis, Uniform interpolation and compact congruences (2016), submitted, https://doi.org/10.1016/j.apal.2017.05.001 · Zbl 1422.03061
[14] J. Hudelmaier, A Prolog program for intuitionistic propositional logic, Tübingen, 1988, SNS-Bericht 88-28.; J. Hudelmaier, A Prolog program for intuitionistic propositional logic, Tübingen, 1988, SNS-Bericht 88-28.
[15] Hudelmaier, J., Bounds for cut elimination in intuitionistic propositional logic, Arch. Math. Logic, 31, 331-353 (1992) · Zbl 0765.03028
[16] Hudelmaier, J., An \(O(n l o g n)\)-space decision procedure for intuitionistic propositional logic, J. Logic Comput., 3, 63-76 (1993) · Zbl 0788.03010
[17] Iemhoff, R., Uniform interpolation and sequent calculi in modal logic, Arch. Math. Logic, 58, 1-2, 155-181 (2019) · Zbl 07006132
[18] Iemhoff, R., Terminating sequent calculi for two intuitionistic modal logics, J. Logic Comput., 28, 7, 1701-1712 (2018) · Zbl 1444.03060
[19] Kremer, On the complexity of propositional quantification in intuitionistic logic, J. Symbolic Logic, 62, 2, 529-544 (1997) · Zbl 0887.03002
[20] Litak, T., Constructive modalities with provability smack, (Bezhanishvili, G., Leo Esakia on Duality in Modal and Intuitionistic Logics. Outstanding Contributions to Logic 4 (2014), Springer), 179-208 · Zbl 1350.03020
[21] Maksimova, L. L., Craig’s theorem in superintuitionistic logics and amalgamated varieties of pseudo-boolean algebras, Algebra Logika, 16, 6, 643-681 (1977) · Zbl 0403.03047
[22] Pitts, A., On an interpretation of second order quantification in first order intuitionistic propositional logic, J. Symbolic Logic, 57, 1, 33-52 (1992) · Zbl 0763.03009
[23] Połacik, T., Pitts’ quantifiers are not topological quantification, Notre Dame J. Form. Log., 39, 4, 531-544 (1998) · Zbl 0966.03008
[24] Shavrukov, V. Y., Subalgebras of Diagonalizable Algebras of Theories Containing Arithmetic, Dissertationes Mathematicae, vol. 323 (1993), Instytut Matematyczny Polskiej Akademi Nauk: Instytut Matematyczny Polskiej Akademi Nauk Warszawa · Zbl 0803.03044
[25] Simpson, A. K., The Proof Theory and Semantics of Intuitionistic Modal Logic (1994), University of Edinburgh, PhD-thesis
[26] Visser, A.; Bisimulations, Model Descriptions and Propositional Quantifiers, Logic Group Preprint Series, vol. 161 (1996), Utrecht University
[27] Visser, A., Uniform interpolation and layered bisimulation, (Hájek, P., Gödel ’96, Logical Foundations of Mathematics, Computer Science and Physics-Kurt Gödel’s Legacy. Gödel ’96, Logical Foundations of Mathematics, Computer Science and Physics-Kurt Gödel’s Legacy, Lecture Notes in Logic, vol. 6 (1996), Springer: Springer Berlin), 139-164 · Zbl 0854.03026
[28] Vorob’ev, N. N., The derivability problem in the constructive propositional calculus with strong negation, Dokl. Akad. Nauk SSSR, 85, 689-692 (1952) · Zbl 0047.25201
[29] Vorob’ev, N. N., A new algorithm for derivability in the constructive propositional calculus, (AMS Translations Ser. 2, vol. 94 (1970)), 37-71 · Zbl 0208.01905
[30] Wolter, F.; Zakharyaschev, M., Intuitionistic modal logic, (Cantini, A.; Casari, E.; Minari, P., Logic and Foundations of Mathematics. Synthese Library, vol. 280 (1999)), 227-238 · Zbl 0955.03029
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.