Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913576002781184 |
|---|---|
| author | Gheorghiu, Alexander V. Gu, Tao Pym, David J. |
| author_facet | Gheorghiu, Alexander V. Gu, Tao Pym, David J. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_05106 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract) Gheorghiu, Alexander V. Gu, Tao Pym, David J. Logic in Computer Science Logic 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. |
| title | Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract) |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2306.05106 |