A Study of Proof-theoretic Harmony in Multilateral Sequent Calculus
Matteo Celli

Abstract:
Bilateralist proof systems, in which the speech acts of assertion and rejection are taken to be both primitive and formulae are presented in assertive and rejective form, have enjoyed a diverse and conspicuous development in the past decades. Not only natural deduction, but sequent calculus formulations have been proposed, and generalisations to more speech acts, giving rise to multilateral systems, have been formulated. Within the field of proof-theoretic semantics, where such proof systems and their underlying philosophical positions are being developed the most, questions arise about how to formulate criterion of why these proof systems can confer meaning, known as harmony criteria. Moreover, an explicit treatment of how to generalise harmony to the multilateralist setting requires further development. In this thesis, I present an account of proof-theoretic harmony to fit a twofold purpose, namely (i) to understand whether coordination principles constitute a bi- and multilateral generalisation of the cut rule and (ii) provide a generalisation of the current literature on harmony suitable to explain what correct use amounts to in multilateral contexts. Turns out that an answer to the more technically-sounding question (i) is highly sensitive to what we take harmony to be, and I defend the view that, if we endorse a broadly Dummettian conception of harmony, for harmony to be an explanatory notion about how meaning arises from use, we should not conflate unilateral, bilateral and multilateral notions of harmony in one single general notion. I will then show how admissibility results of cut and coordination principles enforce these different dimensions of harmony. This, I will argue, means that we should keep a non-trivial distinction between cut and the coordination principles. I will conclude by formulating an account of multilateral harmony and its relation to epistemic modality. This will be carried out in a suitably developed sequent calculus, based on the logics BML and EML presented in (Incurvati and Schlöder, 2023b).