In this talk we provide a complete axiomatization of the Provability Logic for Heyting Arithmetic HA (this is the first-order intuitionistic fragment of the Peano Arithmetic PA). It turns out that the provability logic of HA is equal to iGL (intuitionistic fragment of the Gödel-Löb logic GL) plus ◻A → ◻B for some admissible rules A/B of iGL. Then we describe a crucial tool which was helpful during the completeness proof: a new Kripke style semantic for intuitionistic modal logics, called mixed semantics, which is a combination of derivability and usual validity in Kripke models.
This talk is based on the following two manuscripts: [1, 2].
[1] Mojtaba Mojtahedi. On provability logic of HA, 2022. https://arxiv.org/abs/ 2206.00445.
[2] Mojtaba Mojtahedi. Relative unification in intuitionistic logic: Towards provability logic of HA, 2022. https://arxiv.org/abs/2206.00446.

Zoom room information:
https://us06web.zoom.us/j/81916335336?pwd=5zQT4lutMiBoY5 Xp1pkFGtbqiaGozg.1
Meeting ID: 819 1633 5336
Passcode: 559618