A Sequent Calculus Perspective on Base-Extension Semantics (Technical Report)
By: Victor Barroso-Nascimento, Ekaterina Piotrovskaya, Elaine Pimentel
Potential Business Impact:
Makes computer logic match how we think.
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.
Similar Papers
Base-extension Semantics for Intuitionistic Modal Logics
Logic
Explains how logic rules work by how we use them.
A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
Logic
Connects logic rules to how we prove things.
Proof-theoretic Semantics for Second-order Logic
Logic
Makes logic rules work without needing big math.