A modal provability logic of explicit and implicit proofs

We establish the bi-modal forgetful projection of the Logic of Proofs and Formal Provability GLA. That is to say, we present a normal bi-modal provability logic with modalities □ and ⊠ whose theorems are precisely those formulas for which the implicit provability assertions represented by the ⊠ modality can be realized by explicit proof terms.