Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation

Amirhossein Akbar Tabatabai; Raheleh Jalali

doi:10.1016/j.apal.2026.103814

Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation

Amirhossein Akbar Tabatabai
, Raheleh Jalali

Department of Computer Science

University of Groningen

Research output: Contribution to journal › Article › peer-review

Abstract

In [2], we introduced a syntactically defined and highly general class of calculi known as semi-analytic. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including FLe, FLew, CFLe, and their K, D, and T-type modal extensions, as well as CPC,K, and KD. However, its more striking consequence lies in the negative direction. It extends the negative results of [2] to logics with CIP but without UIP. In particular, it shows that the modal logics and do not have a terminating semi-analytic calculus.

Original language	English
Pages (from-to)	103814
Journal	Annals of Pure and Applied Logic
Volume	178
Issue number	1
Early online date	15 Jul 2026
DOIs	https://doi.org/10.1016/j.apal.2026.103814
Publication status	E-pub ahead of print - 15 Jul 2026

Data Availability Statement

No data was used for the research described in the article.

Acknowledgements

We are grateful to Rosalie Iemhoff for drawing our attention to this intriguing line of research, generously sharing her insights on the topic, and engaging in valuable discussions with us. We also wish to thank Pavel Pudlak, George Metcalfe, Revantha Ramanayake, and Masoud
Memarzadeh for their thoughtful feedback on the initial draft and Hiroakira Ono and Silvio Ghilardi for the helpful discussions we had.

Access to Document

10.1016/j.apal.2026.103814Licence: CC BY

https://linkinghub.elsevier.com/retrieve/pii/S0168007226000977

Cite this

@article{9e9546b4a03745aea5a6bbbfa5a9e360,

title = "Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation",

abstract = "In [2], we introduced a syntactically defined and highly general class of calculi known as semi-analytic. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including FLe, FLew, CFLe, and their K, D, and T-type modal extensions, as well as CPC,K, and KD. However, its more striking consequence lies in the negative direction. It extends the negative results of [2] to logics with CIP but without UIP. In particular, it shows that the modal logics and do not have a terminating semi-analytic calculus.",

author = "Tabatabai, \{Amirhossein Akbar\} and Raheleh Jalali",

year = "2026",

month = jul,

day = "15",

doi = "10.1016/j.apal.2026.103814",

language = "English",

volume = "178",

pages = "103814",

journal = "Annals of Pure and Applied Logic",

issn = "0168-0072",

publisher = "Elsevier B.V.",

number = "1",

}

TY - JOUR

T1 - Universal Proof Theory

T2 - Semi-analytic Rules and Uniform Interpolation

AU - Tabatabai, Amirhossein Akbar

AU - Jalali, Raheleh

PY - 2026/7/15

Y1 - 2026/7/15

N2 - In [2], we introduced a syntactically defined and highly general class of calculi known as semi-analytic. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including FLe, FLew, CFLe, and their K, D, and T-type modal extensions, as well as CPC,K, and KD. However, its more striking consequence lies in the negative direction. It extends the negative results of [2] to logics with CIP but without UIP. In particular, it shows that the modal logics and do not have a terminating semi-analytic calculus.

AB - In [2], we introduced a syntactically defined and highly general class of calculi known as semi-analytic. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including FLe, FLew, CFLe, and their K, D, and T-type modal extensions, as well as CPC,K, and KD. However, its more striking consequence lies in the negative direction. It extends the negative results of [2] to logics with CIP but without UIP. In particular, it shows that the modal logics and do not have a terminating semi-analytic calculus.

U2 - 10.1016/j.apal.2026.103814

DO - 10.1016/j.apal.2026.103814

M3 - Article

SN - 0168-0072

VL - 178

SP - 103814

JO - Annals of Pure and Applied Logic

JF - Annals of Pure and Applied Logic

IS - 1

ER -

Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation

Abstract

Data Availability Statement

Acknowledgements

Access to Document

Fingerprint

Cite this