# Provability Interpretation of Propositional and Modal Logics

## TL;DR

This paper explores formal provability interpretations for propositional and modal logics, generalizing existing frameworks to better understand their foundations and limitations, including the absence of such interpretations for classical logic.

## Contribution

It generalizes Solovay's provability interpretation to multiple modal logics and formalizes the BHK interpretation for various propositional logics, revealing their connections and limitations.

## Key findings

- Provability interpretations exist for some modal and propositional logics.
- No provability interpretation exists for any extension of KD45.
- Classical propositional logic lacks a BHK interpretation.

## Abstract

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.