  The first examples of explicit/implicit knowledge systems appeared in the area of provability logic. In (Sidon 1997, Yavorskaya (Sidon)  2001), a logic \(\mathsf{LPP}\)  was introduced which combined the logic of provability  \(\mathsf{GL}\) with the logic of  proofs \(\mathsf{LP}\), but to  ensure that the resulting system had desirable logical properties  some additional operations from outside the original  languages of \(\mathsf{GL}\) and  \(\mathsf{LP}\) were added. In  (Nogina 2006, Nogina 2007) a complete logical system,  \(\mathsf{GLA}\), for proofs and  provability was offered, in the sum of the original  languages of \(\mathsf{GL}\) and  \(\mathsf{LP}\). Both  \(\mathsf{LPP}\) and  \(\mathsf{GLA}\)  enjoy completeness relative to the  class of arithmetical models, and also relative to the class of  possible world justification models.