 Gödel in “An Interpretation of the Intuitionistic Propositional Calculus” (1933) is the first to propose an alternative axiomatization of the Lewis system S4 that separates the propositional basis of the system from the modal axioms and rules. Gödel adds the following rules and axioms to the propositional calculus. 