 Heyting’s essay covered propositional logic, predicate logic, arithmetic, and Brouwerian set theory or analysis. One would think that, to be able to achieve this, Heyting must have had quite precise ideas on how to explain the logical connectives intuitionistically. However, Heyting’s correspondence with Freudenthal in 1930 shows that before 1930, Heyting had not yet arrived at the explicit requirement of a transformation procedure in the explanation of implication (see the  quotation  in  section 5.1  below).