A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866913938732482560 |
|---|---|
| author | Barroso-Nascimento, Victor Piotrovskaya, Ekaterina Pimentel, Elaine |
| author_facet | Barroso-Nascimento, Victor Piotrovskaya, Ekaterina Pimentel, Elaine |
| contents | We define base-extension semantics (Bes) using atomic systems based on sequent calculus rather than natural deduction. While traditional Bes aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a Bes framework more suited to classical semantics. The harmony in classical sequents leads to straightforward semantic clauses derived solely from right introduction rules. This framework enables a Sandqvist-style completeness proof that extracts a sequent calculus proof from any valid semantic consequence. Moreover, we show that the inclusion or omission of atomic cut rules meaningfully affects the semantics, yet completeness holds in both cases. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_18589 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report) Barroso-Nascimento, Victor Piotrovskaya, Ekaterina Pimentel, Elaine Logic in Computer Science Logic 03F03 F.3.2 We define base-extension semantics (Bes) using atomic systems based on sequent calculus rather than natural deduction. While traditional Bes aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a Bes framework more suited to classical semantics. The harmony in classical sequents leads to straightforward semantic clauses derived solely from right introduction rules. This framework enables a Sandqvist-style completeness proof that extracts a sequent calculus proof from any valid semantic consequence. Moreover, we show that the inclusion or omission of atomic cut rules meaningfully affects the semantics, yet completeness holds in both cases. |
| title | A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report) |
| topic | Logic in Computer Science Logic 03F03 F.3.2 |
| url | https://arxiv.org/abs/2505.18589 |