Logic of proofs
LP\mathcal{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.