A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)
Victor Barroso-Nascimento, Ekaterina Piotrovskaya, Elaine Pimentel

TL;DR
This paper introduces a sequent calculus-based approach to base-extension semantics, bridging constructive and classical logic by analyzing how sequent rules influence semantic completeness and proof extraction.
Contribution
It presents a novel sequent calculus framework for base-extension semantics, demonstrating its suitability for classical logic and establishing completeness results.
Findings
Sequent calculus with multiple conclusions aligns better with classical semantics.
Completeness holds regardless of atomic cut rule inclusion or omission.
Semantic clauses can be derived solely from right introduction rules.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
