Labeled Sequent Calculus and Countermodel Construction for Justification Logics
Meghdad Ghari
TL;DR
The paper develops modular, G3-style labeled sequent calculi for justification logics by internalizing Fitting semantics via world labels and evidence atoms such as $wE(t,A)$ and $wRv$; it proves key syntactic properties (subformula/sublabel, subterm in many systems), invertibility of rules, and admissibility of weakening, contraction, and cut, together with soundness and completeness against F-models. A constructive proof-search framework produces either a derivation or a countermodel via a reduction tree, and termination results are obtained for several logics under finite constant specifications. The framework extends to modal-justification logics and to several alternative semantic models (Fp, Fk, AF), enabling model correspondences and a unified treatment of analytic proof theory across a broad spectrum of justification formalisms. By providing both axiomatic and semantic tools, the approach supports countermodel construction, model-theoretic correspondence, and potential extensions to multi-agent and Kripke-Mitting-style systems, with clear paths for label-free variants via Mkrtychev models.
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.