Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2018
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913913082216448 |
|---|---|
| author | Tabatabai, Amirhossein Akbar Jalali, Raheleh |
| author_facet | Tabatabai, Amirhossein Akbar Jalali, Raheleh |
| contents | In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{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 $\mathsf{FL_e}$, $\mathsf{FL_{ew}}$, $\mathsf{CFL_e}$, $\mathsf{CFL_{ew}}$, and their $K$, $D$, and $T$-type modal extensions, as well as $\mathsf{CPC}$, $\mathsf{K}$, and $\mathsf{KD}$. However, its more striking consequence lies in the negative direction. It extends the negative results of \cite{Craig} to logics with CIP but without UIP. In particular, it shows that the modal logics $\mathsf{K4}$ and $\mathsf{S4}$ do not have a terminating semi-analytic calculus.
\textbf{keywords:} Uniform interpolation, Sequent calculi, Substructural logics, Modal logics, Subexponential modalities |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1808_06258 |
| institution | arXiv |
| publishDate | 2018 |
| record_format | arxiv |
| spellingShingle | Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation Tabatabai, Amirhossein Akbar Jalali, Raheleh Logic in Computer Science Logic In \cite{Craig}, we introduced a syntactically defined and highly general class of calculi known as \emph{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 $\mathsf{FL_e}$, $\mathsf{FL_{ew}}$, $\mathsf{CFL_e}$, $\mathsf{CFL_{ew}}$, and their $K$, $D$, and $T$-type modal extensions, as well as $\mathsf{CPC}$, $\mathsf{K}$, and $\mathsf{KD}$. However, its more striking consequence lies in the negative direction. It extends the negative results of \cite{Craig} to logics with CIP but without UIP. In particular, it shows that the modal logics $\mathsf{K4}$ and $\mathsf{S4}$ do not have a terminating semi-analytic calculus. \textbf{keywords:} Uniform interpolation, Sequent calculi, Substructural logics, Modal logics, Subexponential modalities |
| title | Universal Proof Theory: Semi-analytic Rules and Uniform Interpolation |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/1808.06258 |