Solovay's arithmetical completeness theorem states that the modal logic of provability coincides with the modal logic $\mathbf{GL}$. Hamkins and Löwe studied the modal logical aspects of set theoretic multiverse and proved that the modal logic of forcing is exactly the modal logic $\mathbf{S4.2}$. We explore the interaction between the notions of provability and forcing in terms of modal logic. We introduce the bimodal logic $\mathbf{PF}$ and prove that the modal logic of provability and forcing is exactly $\mathbf{PF}$. We also introduce the bimodal logic $\mathbf{PF}^ω$ and prove that $\mathbf{PF}^ω$ is exactly the modal logic of provability and forcing true in $ω$-models of set theory.