  Based on Brouwer’s understanding of logical truth as provability,  Gödel defined a translation tr\((F)\) of the propositional  formula \(F\) in the intuitionistic language into the language  of classical modal logic: tr\((F)\) is obtained by prefixing  every subformula of \(F\) with the provability modality \(\Box\). Informally speaking, when the usual procedure of determining  classical truth of a formula is applied to tr\((F)\), it will  test the provability (not the truth) of each of \(F\)’s  subformulas, in agreement with Brouwer’s ideas. From Gödel’s  results and the McKinsey-Tarski work on topological semantics for  modal logic, it follows that the translation tr\((F)\) provides  a proper embedding of the Intuitionistic Propositional Calculus,  \(\mathsf{IPC}\), into  \(\mathsf{S4}\), i.e., an embedding of  intuitionistic logic into classical logic extended by the provability operator.