Interactions and Complexity in Multi-Agent Justification Logic

Justification cation Logic is the logic which introduces justifications to the epistemic setting. In contrast to Modal Logic, when an agent believes (or knows) a certain claim, in Justification Logic we assume the agent believes the claim because of a certain justification. Therefore, instead of having formulas that represent the belief of a claim (ex. □ø or Kø), we have formulas that represent that the belief of a claim follows from a provided justification (ex. t : ø). The original Justification Logic is LP, the Logic of Proofs, and was introduced by Artemov in 1995 as a link between Intuitionistic Truth and Gödel proofs in Peano Arithmetic. The complexity of Justification Logic was first studied by Kuznets in 2000. He demonstrated that for many justification logics, their derivability problem (and thus their satisfiability problem) is in the second level of the Polynomial Hierarchy, a result which was shown to be tight and which was later extended to more justification logics. In fact, so far, given reasonable assumptions, every single-agent justification logic whose complexity has been settled has its satisfiability problem in the second level of the Polynomial Hierarchy. This result is nicely contrasted to Modal Logic, as the corresponding modal systems are PSPACE-complete. We investigate the complexity of Justification Logic and Modal Logic when we allow multiple agents whose justifications affect each other -- by including some combination of the axioms t :iø → t :jø and t :iø → !t :j t :iø (modal cases: □iø→ □jø). We discover complexity jumps new for the field of Justification Logic: in addition to logics with their satisfiability problem in the second level of the polynomial hierarchy (as is the usual case until now), there are logics that have PSPACE-complete, EXP-complete and even NEXP-complete satisfiability problems. It is notable how the behavior of several of these justification logics mirrors the behavior of the corresponding multi-modal logics when we restrict modal formulas (in negation normal form) to use no diamonds. Thus we first study the complexity of such diamond-free modal logics and then we deduce complexity properties for the justification logic systems. On the other hand, it is similarly notable how certain lower complexity bounds -- the NEXP-hardness bound and the general Σp2-hardness bound we present -- are more dependent on the behavior of the justifications. The complexity results are interesting for Modal Logic as well, as we give hardness results that hold even for the diamond-free, 1-variable fragments of these multi-modal logics and then we determine the complexity of these logics in a general case