Analytic Tableaux for Justification Logics

TL;DR

This paper introduces analytic tableau proof systems for justification logics, demonstrating their soundness, completeness, and decidability, with a focus on syntactic cut elimination and subformula properties.

Contribution

It provides the first tableau systems for justification logics, establishing soundness, completeness, and decidability results with a syntactic proof framework.

Findings

Tableau systems are sound and complete for justification logics.

Decidability is proven for finite constant specifications.

Syntactic cut elimination and subformula property are established.

Abstract

In this paper we present analytic 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, and prove the decidability of justification logics for finite constant specifications.