Tableau Proof Systems for Justification Logics
Meghdad Ghari
TL;DR
The paper develops two tableau proof systems for each justification logic ${\sf JL}$ and proves their soundness and completeness with respect to Mkrtychev models. The first system ${\sf JL}_{\mathcal{CS}}$-tableaux mirrors Renne’s LP-style tableaux, while the second system ${\sf JL}^{\mathcal{T}}_{\mathcal{CS}}$-tableaux adopts analytic, KE-inspired rules with a restricted $(PB)$ rule and uses cut elimination to achieve completeness alongside a defined subformula property. Key contributions include deriving two complementary tableau frameworks, establishing soundness and completeness results, and proving cut-elimination for the analytic system, which yields analytic tableaux under suitable restrictions. The work advances proof-theoretic methods for justification logics and connects tableau techniques to semantic models for justification, enabling more robust automated reasoning within this logical family.
Abstract
In this paper we present tableau proof systems for various justification logics. We show that the tableau systems are sound and complete with respect to Mkrtychev models. In order to prove the completeness of the tableaux, we give a syntactic proof of cut elimination. We also show the subformula property for our tableaux.