Barroso-Nascimento, Victor;
Piotrovskaya, Ekaterina;
Pimentel, Elaine;
(2025)
A Sequent Calculus Perspective on Base-Extension Semantics.
In:
Automated Reasoning with Analytic Tableaux and Related Methods.
(pp. pp. 3-21).
Springer Nature: Cham, Switzerland.
Preview |
Text
978-3-032-06085-3_1 (3).pdf - Published Version Download (438kB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | A Sequent Calculus Perspective on Base-Extension Semantics |
| Dates: | 27th September - 2nd October 2025 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-032-06085-3_1 |
| Publisher version: | https://doi.org/10.1007/978-3-032-06085-3_1 |
| Language: | English |
| Additional information: | © 2026 The Author(s). This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/). The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10216280 |
Archive Staff Only
 |
View Item |
