Uploaded November 2025 | Updated September 2026, 1 hour ago
Recorded as part of the CFvW Colloquium on November 5, 2025
A B-eS approach to Bilateralism - Maria Osório Costa (Universidade de Lisboa and University College London)
Abstract:
This presentation introduces two recent developments in bilateral proof-theoretic semantics. We first outline an extension of base-extension semantics (B-eS) to the bilateral setting, yielding a semantics sound and complete with respect to N2Int*, a modified version of Wansing’s natural-deduction system for the bilateral bi-intuitionistic logic 2Int. The extension is achieved by allowing atomic bases to contain both proof and refutation rules, thereby capturing the bilateralist idea that assertion and denial are independent acts. We then turn to the notion of incompatibility between proofs and refutations, something naturally expected in settings such as mathematical reasoning. By enriching N2Int* with suitable interaction rules, we obtain BPR, a system that enjoys normalization, the subformula principle, and consistency. A refined bilateral B-eS semantics, defined over restricted bases, captures this incompatibility at the semantic level. Finally, we show that BPR is intimately connected with Nelson’s concept of constructive falsity, as it internalizes falsity through the notion of refutation.
Recorded as part of the CFvW Colloquium on November 5, 2025
A B-eS approach to Bilateralism - Maria Osório Costa (Universidade de Lisboa and University College London)
Abstract:
This presentation introduces two recent developments in bilateral proof-theoretic semantics. We first outline an extension of base-extension semantics (B-eS) to the bilateral setting, yielding a semantics sound and complete with respect to N2Int*, a modified version of Wansing’s natural-deduction system for the bilateral bi-intuitionistic logic 2Int. The extension is achieved by allowing atomic bases to contain both proof and refutation rules, thereby capturing the bilateralist idea that assertion and denial are independent acts. We then turn to the notion of incompatibility between proofs and refutations, something naturally expected in settings such as mathematical reasoning. By enriching N2Int* with suitable interaction rules, we obtain BPR, a system that enjoys normalization, the subformula principle, and consistency. A refined bilateral B-eS semantics, defined over restricted bases, captures this incompatibility at the semantic level. Finally, we show that BPR is intimately connected with Nelson’s concept of constructive falsity, as it internalizes falsity through the notion of refutation.
