 Initially, Gödel employs an operator \(B\) of provability to translate Heyting’s primitive intuitionistic connectives, and then observes that if we replace \(B\) with an operator of necessity we obtain the system S4. Gödel also claims that a formula \(\Box p\vee \Box q\) is not provable in S4 unless either \(\Box p\) or \(\Box q\) is provable, analogously to intuitionistic disjunction. Gödel’s claim will be proved algebraically by McKinsey and Tarski (1948). Gödel’s short note is important for starting the fruitful practice of axiomatizing modal systems separating the propositional calculus from the strictly modal part, but also for connecting intuitionistic and modal logic.