A Proof-Theoretic Approach to the Semantics of Classical Linear Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915823774334976 |
|---|---|
| author | Barroso-Nascimento, Victor Piotrovskaya, Ekaterina Pimentel, Elaine |
| author_facet | Barroso-Nascimento, Victor Piotrovskaya, Ekaterina Pimentel, Elaine |
| contents | Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces).
This work proposes a different perspective on assigning meaning to proofs by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support.
Recent developments have shown that BeS is powerful enough to capture proof-theoretic notions in structurally rich logics such as intuitionistic linear logic. In this paper, we extend this framework to the classical case, presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic (MALL). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_08349 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Proof-Theoretic Approach to the Semantics of Classical Linear Logic Barroso-Nascimento, Victor Piotrovskaya, Ekaterina Pimentel, Elaine Logic in Computer Science Logic 03F03 F.4.1; F.3.2 Linear logic (LL) is a resource-aware, abstract logic programming language that refines both classical and intuitionistic logic. Linear logic semantics is typically presented in one of two ways: by associating each formula with the set of all contexts that can be used to prove it (e.g. phase semantics) or by assigning meaning directly to proofs (e.g. coherence spaces). This work proposes a different perspective on assigning meaning to proofs by adopting a proof-theoretic perspective. More specifically, we employ base-extension semantics (BeS) to characterise proofs through the notion of base support. Recent developments have shown that BeS is powerful enough to capture proof-theoretic notions in structurally rich logics such as intuitionistic linear logic. In this paper, we extend this framework to the classical case, presenting a proof-theoretic approach to the semantics of the multiplicative-additive fragment of linear logic (MALL). |
| title | A Proof-Theoretic Approach to the Semantics of Classical Linear Logic |
| topic | Logic in Computer Science Logic 03F03 F.4.1; F.3.2 |
| url | https://arxiv.org/abs/2504.08349 |