Intuitionistic provability logic

Provability logic studies formal notions of provability through the language of modal logic, interpreting the modal operator as "provability in a fixed mathematical theory’’. The celebrated theorems of Löb and Solovay show that the propositional provability logic of every sufficiently strong and sufficiently sound classical theory is exactly the Gödel–Löb logic $\mathsf{GL}$. The intuitionistic setting is markedly more subtle, largely because of the existence of admissible but non-derivable rules of inference. In this talk, we survey the research program initiated by Albert Visser and developed by the Dutch school, whose central goal is a complete axiomatization and a decidability theorem for the provability logic of Heyting Arithmetic ($\mathsf{HA}$). We discuss several of the key ideas and techniques involved, including {NNIL} formulas, unification, projectivity, and admissible rules of intuitionistic logic. We explain how these notions interact in the study of $\mathsf{HA}$-provability, and how the research around them has also provided a positive impetus to the study of admissible rules in intuitionistic logic. The talk concludes with recent progress toward the complete axiomatization and decidability of $\mathsf{HA}$-provability logic.