GroLog Seminar

SPEAKER: AmirHossein Akbar Tabatabai (University of Groningen)

DATE: Thu 1 June 2023

TIME: 16:00-17:00

PLACE: Room 293 in the BernoulliBorg building (Room 5161.0293)

TITLE: A Provability Interpretation for some Propositional and Modal Logics

ABSTRACT:  In 1933, to establish a formalization for the BHK interpretation, Gödel introduced a provability interpretation for the intuitionistic propositional logic, IPC, reading the intuitionistic constructions as the usual classical proofs. Instead of using any concrete notion of a proof, he used the modal system S4 as a formalization for the intuitive concept of provability and then translated IPC into S4 in a sound and complete manner. This translation then reduced the formalization of the BHK interpretation to finding a concrete provability interpretation for the modal logic S4. 

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 GL to capture other modal logics such as K4, KD4 and 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 some extensions of 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 KD45, and as expected, there is no BHK interpretation for the classical propositional logic.