Gödel's modal interpretation of intuitionistic logic and its proof theory

Gödel, working within axiomatic logic, succeeded in 1933 in establishing a translation from theorems of intuitionistic propositional logic to ones of classical logic enriched with a modal provability operator. The converse correspondence was established by semantical means in 1948, and by Gödel through a syntactic translation in unpublished work of 1941. It is shown through proof analysis of formal derivations in natural deduction for modal logic that steps of indirect proof in normal derivations of translations of intuitionistic formulas are vacuous. This conservativity of classical over intuitionistic modal logic for translated formulas is the reason why Gödel's modal translation succeeds in singling out a "provability fragment" within classical modal logic that coincides with intuitionistic logic.