Provability as a Modality

Notes from discussion on Section 2.4 Gödel on Provability as a Modality from Goldblatt's paper Mathematical Modal Logic: A View of Its Evolution

Gödel in his paper An interpretation of the intuitionistic propositional calculus made formal assertions of provability using the propositional connective B. For example, if some propositional statement a was provable, we would write Ba. He defined a system of logic by adding the following three axioms to ordinary propositional calculus.

He also added the inference rule: from a infer Ba. In other words, if a is true then you know that a is provable. This statement is along the lines of intuitionistic logic. The first and third rules merely provide a way to add or remove the connective B.