 Gödel considers intuitionistic propositional logic (henceforth IPL); he also considers a second system, classical propositional logic enriched by an operator “B”, where the intended meaning of “B” is “provable.” The axiom system now known as S4 (for a list of these axioms see for example the entry on  modal logic  in this encyclopedia) is added to the standard axioms for classical propositional logic together with a new rule of proof: from A, BA may be inferred. Let us call this second system G. Gödel’s theorem states that IPL is interpretable in G via the following translation: