Provability Interpretation of Propositional and Modal Logics

In 1933, G\"odel introduced a provability interpretation of the propositional intuitionistic logic to establish a formalization for the BHK interpretation. He used the modal system, $\mathbf{S4}$, as a formalization of the intuitive concept of provability and then translated $\mathbf{IPC}$ to $\mathbf{S4}$. His work suggested the problem to find a concrete provability interpretation of the modal logic $\mathbf{S4}$. In this paper, we will try to answer this problem. In fact, we will generalize Solovay's provability interpretation of the modal logic $\mathbf{GL}$ to capture other modal logics such as $\mathbf{K4}$, $\mathbf{KD4}$ and $\mathbf{S4}$. Then we will use these results to find a formalization for the BHK interpretation and we will show that with different interpretations of the BHK interpretation, we can capture some of the propositional logics such as Intuitionistic logic, minimal logic and Visser-Ruitenburg's basic logic. Moreover, we will show that there is no provability interpretation for any extension of $\mathbf{KD45}$ and also there is no BHK interpretation for the classical propositional logic.