Bilateral base-extension semantics
Victor Barroso-Nascimento, Maria Osório
TL;DR
This paper develops bilateral base-extension semantics ($\sf{BeS}$) for the bilateral logic $2Int$, where atomic bases can contain both atomic proof and refutation rules. By introducing bilateral atomic systems, deductions, and semantic clauses, the authors define a semantic framework in terms of proofs and refutations, and prove soundness and completeness with respect to $2Int$ via a Sandqvist-style construction. A central innovation is the duality of rules, deductions, and bases, which underpins a semantic version of the horizontal inversion principle and yields bilateral semantic harmony (both weak and strong). The work also clarifies how the semantics can embed across language fragments and demonstrates that the deductively equivalent system $\sf{N2Int}$ does not always align with the underlying semantic notions, whereas $\sf{N2Int^*}$ does, guiding future intertwining of proof-theoretic semantics with semantic harmony insights.
Abstract
Bilateralism is the position according to which assertion and rejection are conceptually independent speech acts. Logical bilateralism demands that systems of logic provide conditions for assertion and rejection that are not reducible to each other, which often leads to independent definitions of proof rules (for assertion) and dual proof rules, also called refutation rules (for rejection). Since it provides a critical account of what it means for something to be a proof or a refutation, bilateralism is often studied in the context of proof-theoretic semantics, an approach that aims to elucidate both the meaning of proofs (and refutations) and what kinds of semantics can be given if proofs (and refutations) are considered as basic semantic notions. The recent literature on bilateral proof-theoretic semantics has only dealt with the semantics of proofs and refutations, whereas we deal with semantics in terms of proofs and refutations. In this paper we present a bilateral version of base-extension semantics - one of the most widely studied proof-theoretic semantics - by allowing atomic bases to contain both atomic proof rules and atomic refutation rules. The semantics is shown to be sound and complete with respect to the bilateral dual intuitionistic logic 2Int. Structural similarities between atomic proofs and refutations also allow us to define duality notions for atomic rules, deductions and bases, which may then be used for the proof of bilateral semantic harmony results. Aside from enabling embeddings between different fragments of the language, bilateral semantic harmony is shown to be a restatement of the syntactic horizontal inversion principle, whose meaning-conferring character may now be interpreted as the requirement of preservation of harmony notions already present at the core of the semantics by inferences.