A complexity question in justification logic

•We examine the complexity of satisfiability for justification logic JD4.•We prove completeness of this logic with respect to Fitting models of two states.•Based on these semantics we give a tableau procedure for JD4.•We conclude that satisfiability is in Σ2p under reasonable conditions.•We thus tighten the lower bound by Buss and Kuznets.

Bounds for the computational complexity of major justification logics were found in papers by Buss, N. Krupski, Kuznets, and Milnikel: logics J, J4, JT, LP and JD were established to be Σ2p-complete. A corresponding lower bound is also known for JD4, the system that includes the consistency axiom and positive introspection. However, no upper bound has been established so far for this logic. Here, the missing upper bound for the complexity of JD4 is established through an alternating algorithm. It is shown that using Fitting models of only two worlds is adequate to describe JD4; this helps to design an effective tableau procedure and essentially is what distinguishes the new algorithm from existing ones.