On the Proof Theory of Inquisitive Logic
Valentin Müller

Abstract:
This thesis is a proof-theoretical study of various systems of inquisitive logic. In the first part, we consider the basic system of propositional inquisitive logic, denoted by InqB (see, e.g., Ciardelli 2022). We construct a natural deduction system for InqB, prove a normalization theorem and establish a restricted subformula property. Our system is based on an extended natural deduction formalism in which not only formulas, but also rules can act as assumptions that may be discharged in the course of a derivation. We then present a G3-style labelled sequent calculus with internalized support semantics for InqB. Our system is shown to satisfy a number of convenient structural properties such as cut-admissibility, height-preserving admissibility of weakening and contraction, and height-preserving invertibility of all rules. Afterwards, we modularly adapt our sequent calculus to other systems of inquisitive logic, including an intuitionistic variant of InqB described by Ciardelli et al. (2020) and extensions of InqB with Kripke modalities. We provide a general method that allows to construct cut-free labelled sequent calculi for all inquisitive Kripke logics characterized by a certain type of first-order formulas, known as geometric implications. This generalizes a famous result for ordinary modal logic established by Negri (2005).