0598219 - MÚ 2026 RIV NL eng J - Journal Article
Akbar Tabatabai, Seyed Amirhossein - Jalali Keshavarz, Raheleh
Universal proof theory: Semi-analytic rules and Craig interpolation.
Annals of Pure and Applied Logic. Roč. 176, č. 1 (2025), č. článku 103509. ISSN 0168-0072. E-ISSN 1873-2461
R&D Projects: GA ČR(CZ) GA23-04825S; GA ČR(CZ) GA22-01137S
Institutional support: RVO:67985840 ; RVO:67985807
Keywords : Craig interpolation * linear logics * sequent calculi
OECD category: Pure mathematics
Impact factor: 0.6, year: 2023 ; AIS: 0.578, rok: 2023
Method of publishing: Limited access
Result website:
https://doi.org/10.1016/j.apal.2024.103509DOI: https://doi.org/10.1016/j.apal.2024.103509

We provide a general and syntactically defined family of sequent calculi, called semi-analytic, to formalize the informal notion of a “nice” sequent calculus. We show that any sufficiently strong (multimodal) substructural logic with a semi-analytic sequent calculus enjoys the Craig Interpolation Property, CIP. As a positive application, our theorem provides a uniform and modular method to prove the CIP for several multimodal substructural logics, including many fragments and variants of linear logic. More interestingly, on the negative side, it employs the lack of the CIP in almost all substructural, superintuitionistic and modal logics to provide a formal proof for the well-known intuition that almost all logics do not have a “nice” sequent calculus. More precisely, we show that many substructural logics including UL−, MTL, R, Łn (for n⩾3), Gn (for n⩾4), and almost all extensions of IMTL, Ł, BL, RMe, IPC, S4, and Grz (except for at most 1, 1, 3, 8, 7, 37, and 6 of them, respectively) do not have a semi-analytic calculus.
Permanent Link: https://hdl.handle.net/11104/0355944