 Heyting told van Dalen that he had the notion of (intuitionistic) construction in mind to guide him in devising his formalization of intuitionistic logic and mathematics in 1927. In the published version of his formalization, he did not elaborate much on the meaning of the connectives; all he explained there about the general meaning of \(a \rightarrow b\) was that “If \(a\) is correct, then \(b\) is correct too” (Heyting 1930: 44 [Mancosu 1998: 313]). Correspondence between Heyting and Freudenthal in 1930 shows that Heyting up till then did not have a more refined explanation at hand; we will come back to this later in this section.