Amir Hossein Akbar Tabatabai
Utrecht University

In 1933, Gödel introduced a provability interpretation for intuitionistic propositional logic, \(\mathbf{IPC}\), to establish a formalization for the BHK interpretation, reading intuitionistic constructions as the usual classical proofs [1]. However, instead of using any concrete notion of a proof, he used the modal system \(\mathbf{S4}\), as a formalization for the intuitive concept of provability and then translated \(\mathbf{IPC}\) into \(\mathbf{S4}\) in a sound and complete manner. His work then suggested the problem to find the missing concrete provability interpretation of the modal logic \(\mathbf{S4}\) to complete his formalization of the BHK interpretation via classical proofs.

In this talk, we will develop a framework for such provability interpretations. We will first generalize Solovay's seminal provability interpretation of the modal logic \(\mathbf{GL}\) to capture other modal logics such as \(\mathbf{K4}\), \(\mathbf{KD4}\) and \(\mathbf{S4}\). The main idea is introducing a hierarchy of arithmetical theories to represent the informal hierarchy of meta-theories of the discourse and then interpreting the nested modalities in the language as the provability predicates of the different layers of this hierarchy. Later, we will combine this provability interpretation with Gödel's translation to propose a classical formalization for the BHK interpretation. The formalization suggests that the BHK interpretation is nothing but a plural name for different provability interpretations for different propositional logics based on different ontological commitments that we believe in. They include intuitionistic logic, minimal logic and Visser-Ruitenburg's basic logic. Finally, as a negative result, we will first show that there is no provability interpretation for any extension of the logic \(\mathbf{KD45}\), and as expected, there is no BHK interpretation for the classical propositional logic.

[1] K. Gödel, Eine Interpretation des Intuitionistichen Aussagenkalküls, Ergebnisse Math Colloq., vol. 4 (1933), pp. 39-40.