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

Publication date: 12 August 2021

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.

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)

This page was built for publication: Normalisation for Bilateral Classical Logic with some Philosophical Remarks, and a Note on it

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6375103)