Gheorghiu, Alexander V;
Gu, Tao;
Pym, David G;
(2023)
Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract).
In:
Proceedings of the 7th International Workshop on Trends in Linear Logic and Applications (TLLA 2023).
7th International Workshop on Trends in Linear Logic and Applications (TLLA 2023): Rome, Italy.
Preview |
Text
Pym_tlla-2023.pdf Download (274kB) | Preview |
Abstract
This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist’s B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for (IMLL), in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.
| Type: | Proceedings paper |
|---|---|
| Title: | Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract) |
| Event: | 7th International Workshop on Trends in Linear Logic and Applications (TLLA 2023) |
| Open access status: | An open access version is available from UCL Discovery |
| Publisher version: | https://lipn.univ-paris13.fr/TLLA/2023/ |
| Language: | English |
| Additional information: | This version is the author-accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | Logic, Semantics, Proof Theory, Proof-theoretic Semantics, Substructural Logic, Multiplicative Connectives |
| 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-pp.ucl.ac.uk/id/eprint/10176107 |
Archive Staff Only
 |
View Item |
