arXiv · 1401.1065
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
Abstract
Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for hybrid modal-justification logics. Using the method due to Sara Negri, we internalize the Kripke-style semantics of justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculus. We show that our labeled sequent calculi enjoy a weak subformula property, all of the rules are invertible and the structural rules (weakening and contraction) and cut are admissible. Finally soundness and completeness are established, and termination of proof search for some of the labeled systems are shown. We describe a procedure, for some of the labeled systems, which produces a derivation for valid sequents and a countermodel for non-valid sequents. We also show a model correspondence for justification logics in the context of labeled sequent calculus.
Explore related subjects
Keep this discovery
Meghdad Ghari. 2014-01-06. Labeled Sequent Calculus and Countermodel Construction for Justification Logics. https://doi.org/10.1016/j.apal.2016.08.006
Cite the original work for its findings. Save a collection to share your selection of sources.