We define base-extension semantics ( \(\textsf{BeS}\) ) using atomic systems based on sequent calculus rather than natural deduction. While traditional \(\textsf{BeS}\) aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a \(\textsf{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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Sequent Calculus Perspective on Base-Extension Semantics

  • Victor Barroso-Nascimento,
  • Ekaterina Piotrovskaya,
  • Elaine Pimentel

摘要

We define base-extension semantics ( \(\textsf{BeS}\) ) using atomic systems based on sequent calculus rather than natural deduction. While traditional \(\textsf{BeS}\) aligns naturally with intuitionistic logic due to its constructive foundations, we show that sequent calculi with multiple conclusions yield a \(\textsf{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.