Universal Proof Theory: Semi-analytic Rules and Craig Interpolation
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2018
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929482699374592 |
|---|---|
| author | Tabatabai, Amirhossein Akbar Jalali, Raheleh |
| author_facet | Tabatabai, Amirhossein Akbar Jalali, Raheleh |
| contents | We provide a general and syntactically-defined family of sequent calculi, called \emph{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 $\mathsf{UL^-}$, $\mathsf{MTL}$, $\mathsf{R}$, $\mathsf{L}_n$ (for $n \geq 3$), $\mathsf{G}_n$ (for $n \geq 4$), and almost all extensions of $\mathsf{IMTL}$, $\mathsf{L}$, $\mathsf{BL}$, $\mathsf{RM^e}$, $\mathsf{IPC}$, $\mathsf{S4}$, and $\mathsf{Grz}$, (except for at most 1, 1, 3, 8, 7, 37, and 6 of them, respectively) do not have a semi-analytic calculus.
Keywords. Craig interpolation, sequent calculi, substructural logics, linear logics, subexponential modalities |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1808_06256 |
| institution | arXiv |
| publishDate | 2018 |
| record_format | arxiv |
| spellingShingle | Universal Proof Theory: Semi-analytic Rules and Craig Interpolation Tabatabai, Amirhossein Akbar Jalali, Raheleh Logic in Computer Science Logic We provide a general and syntactically-defined family of sequent calculi, called \emph{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 $\mathsf{UL^-}$, $\mathsf{MTL}$, $\mathsf{R}$, $\mathsf{L}_n$ (for $n \geq 3$), $\mathsf{G}_n$ (for $n \geq 4$), and almost all extensions of $\mathsf{IMTL}$, $\mathsf{L}$, $\mathsf{BL}$, $\mathsf{RM^e}$, $\mathsf{IPC}$, $\mathsf{S4}$, and $\mathsf{Grz}$, (except for at most 1, 1, 3, 8, 7, 37, and 6 of them, respectively) do not have a semi-analytic calculus. Keywords. Craig interpolation, sequent calculi, substructural logics, linear logics, subexponential modalities |
| title | Universal Proof Theory: Semi-analytic Rules and Craig Interpolation |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/1808.06256 |