Universal proof theory: Semi-analytic rules and Craig interpolation
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F25%3A00598219" target="_blank" >RIV/67985840:_____/25:00598219 - isvavai.cz</a>
Alternative codes found
RIV/67985807:_____/25:00598219
Result on the web
<a href="https://doi.org/10.1016/j.apal.2024.103509" target="_blank" >https://doi.org/10.1016/j.apal.2024.103509</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.apal.2024.103509" target="_blank" >10.1016/j.apal.2024.103509</a>
Alternative languages
Result language
angličtina
Original language name
Universal proof theory: Semi-analytic rules and Craig interpolation
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Annals of Pure and Applied Logic
ISSN
0168-0072
e-ISSN
1873-2461
Volume of the periodical
176
Issue of the periodical within the volume
1
Country of publishing house
NL - THE KINGDOM OF THE NETHERLANDS
Number of pages
26
Pages from-to
103509
UT code for WoS article
001307686700001
EID of the result in the Scopus database
2-s2.0-85202691079