Normalisation for Bilateral Classical Logic with some Philosophical Remarks, and a Note on it

TL;DR

This paper develops a normalization theorem for bilateral classical logic, introduces new bilateral connectives, and discusses philosophical implications and issues related to coherence and stability in bilateral logic systems.

Contribution

It presents a normalization proof for bilateral classical logic and introduces two new bilateral connectives with reduction steps, addressing coherence problems.

Findings

Normalization theorem established for bilateral logic

Two new bilateral connectives with reduction steps introduced

Discussion on philosophical implications and coherence issues

Abstract

Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. The Note corrects an error in one of the reduction steps in the paper.