Propositional quantifiers in labelled natural deduction for normal modal logic

This article concerns the treatment of propositional quantification in a framework of labelled natural deduction for modal logic developed by Basin, Matthews and Vigano. We provide a detailed analysis of a basic calculus that can be used for a proof-theoretic rendering of minimal normal multimodal systems with quantification over stable domains of propositions. Furthermore, we consider variations of the basic calculus obtained via relational theories and domain theories allowing for quantification over possibly unstable domains of propositions. The main result of the article is that fragments of the labelled calculi not exploiting reductio ad absurdum enjoy the Church-Rosser property and the strong normalization property; such result is obtained by combining Girard's method of reducibility candidates and labelled languages of lambda calculus codifying the structure of modal proofs.