Multi-agent explicit knowledge

Logic of proofs LP, introduced by S. Artemov, originally designed for describing properties of formal proofs, now became a basis for the theory of knowledge with justification. So far, in epistemic systems with justification the corresponding "evidence part", even for multi-agent systems, consisted of a single explicit evidence logic. In this paper we introduce logics describing two interacting explicit evidence systems. We find an appropriate formalization of the intended semantics and prove the completeness of these logics with respect to both symbolic and arithmetical models. Also, we find the forgetful projections for the logics with two proof predicates which are extensions of the bimodal logic S4(2).