Xavier, Bruno;
Olarte, Carlos;
Pimentel, Elaine;
(2022)
A linear logic framework for multimodal logics.
Mathematical Structures in Computer Science
pp. 1-29.
10.1017/s0960129522000366.
(In press).
Preview |
PDF
a-linear-logic-framework-for-multimodal-logics.pdf - Published Version Download (542kB) | Preview |
Abstract
One of the most fundamental properties of a proof system is analyticity, expressing the fact that a proof of a given formula F only uses subformulas of F. In sequent calculus, this property is usually proved by showing that the cut rule is admissible, i.e., the introduction of the auxiliary lemma H in the reasoning “if H follows from G and F follows from H, then F follows from G” can be eliminated. The proof of cut admissibility is usually a tedious, error-prone process through several proof transformations, thus requiring the assistance of (semi-)automatic procedures. In a previous work by Miller and Pimentel, linear logic (LL) was used as a logical framework for establishing sufficient conditions for cut admissibility of object logical systems (OL). The OL’s inference rules are specified as an LL theory and an easy-to-verify criterion sufficed to establish the cut-admissibility theorem for the OL at hand. However, there are many logical systems that cannot be adequately encoded in LL, the most symptomatic cases being sequent systems for modal logics. In this paper, we use a linear-nested sequent (LNS) presentation of MMLL (a variant of LL with subexponentials), and show that it is possible to establish a cut-admissibility criterion for LNS systems for (classical or substructural) multimodal logics. We show that the same approach is suitable for handling the LNS system for intuitionistic logic.
| Type: | Article |
|---|---|
| Title: | A linear logic framework for multimodal logics |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1017/s0960129522000366 |
| Publisher version: | https://doi.org/10.1017/S0960129522000366 |
| Language: | English |
| Additional information: | © The Author(s) 2022. Published by Cambridge University Press. This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/). |
| Keywords: | Linear logic; cut elimination; multimodal logics; linear-nested systems |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10161307 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
