Multilateral calculi for free-choice logics
Edoardo Menorello

Abstract:
This dissertation is a proof-theoretical investigation on some variants of free-choice logics from the standpoint of inferential expressivism.
The phenomenon of free-choice inference has been recently studied in the context of team semantics, starting with [Alo22]. Advancements in this tradition have mostly relied on model-theoretical approaches, and, while those have been successful in offering predictions for natural-language phenomena such as free-choice permissions ([Kam13]) and epistemic contradictions ([Yal07]), the development of proof-systems connected to these logics has been slower and not always fully satisfactory. In particular, axiomatizations for logics not admitting the empty set as a licit team have not yet been investigated. This work offers axiomatizations for two such logics BSL^V_m and BSL_m, in the style of multilateral calculi developed in the context of Inferential expressivism ([IS23]).
After studying some model-theoretical properties, a natural deduction system for BSL^V_m is outlined, and an interpretation of the logic from the perspective of inferential expressivism is given. In particular, the system is shown to comply with proof-theoretic harmony in the form of local soundness and completeness. As a result, specific constants employs BSL^V_m, to model phenomena as epistemic contradictions and free-choice permissions are shown to qualify as meaning-determining connectives, from the standpoint of an inferentialist theory of meaning. The system is then shown to be sound and complete, and a normal form result together with a weak subformula property is offered. Last, a labelled sequent system for the sub-logic BSL_m is outlined, together with results of soundness, completeness, and proof-search termination.