Labeled Sequent Calculus and Countermodel Construction for Justification Logics

TL;DR

This paper develops labeled sequent calculi for justification logics, enabling internalization of Kripke-style semantics, and provides methods for proof search, derivation, and countermodel construction.

Contribution

It introduces a novel labeled sequent calculus framework for justification logics, integrating semantics into syntax and establishing soundness, completeness, and proof search procedures.

Findings

Labeled sequent calculi enjoy weak subformula property

Rules are invertible and structural rules are admissible

Proof search terminates for some systems and countermodels can be constructed

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.