Marco Volpe (INRIA)

Focused proofs are sequent calculus proofs that group inference rules into alternating positive and negative phases. These phases can then be used to define macro-level inference rules from Gentzen’s original and tiny introduction and structural rules. In this talk, I will show that the inference rules of labeled proof systems for modal logics can similarly be described as pairs of such positive and negative phases within focused proof system for first-order classical logic. In particular, I will consider the system G3K of Negri for the modal logic K and define a translation from labeled modal formulas into first-order polarized formulas and show a strict correspondence between derivations in the two systems, i.e., each rule application in G3K corresponds to a bipole (a pair of a positive and a negative phases) in the focused system. Since geometric axioms (when properly polarized) induce bipoles, this strong correspondence holds for all modal logics whose Kripke frames are characterized by geometric properties. These results can be extended to present a focused labeled proof system for the same class of modal logics and show its soundness and completeness. (Joint work with Dale Miller.)