Tableaux and hypersequents for justification logic

Abstract

Justification Logic is a new generation of epistemic logics which along with the traditional modal knowledge/belief operators also consider justification assertions 't is a justification for F.' In this paper, we introduce a prefixed tableau system for one of the major logics of this kind S4LPN, which combines the logic of proofs (LP) and epistemic logic S4 with an explicit negative introspection principle ¬t :F → ;¬t :F. We show that the prefixed tableau system for S4LPN is sound and complete with respect to Fitting-style semantics. We also introduce a hypersequent calculus HS4LPN and show that HS4LPN is complete as far as we confine ourselves to a case where only a single formula is to be proven. We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus. This completeness result gives us a semantic proof of cut-admissibility for S4LPN under the aforementioned restriction. © Springer-Verlag Berlin Heidelberg 2009.