1. The locus classicus here is Tarski 1953. A recent treatment of formalized interpretability is Joosten 2004.

2. One will want to impose various (structural) constraints on the interpretation, to avoid trivial ones that map for example all formulas of U to an axiom of V.

3. Whenever a specific page is referred to of a text that is originally not in English, a reference to the corresponding page of an English translation, if available, is given as well.

4. This is subjective time (one may think here of Husserl’s notion of inner time consciousness) rather than objective or scientific time (time as it figures in physics and that one measures with a clock); the latter, according to Brouwer, presupposes mathematics (Brouwer 1907: 99n.2 [1975: 61n.2]).

5. The Collected Works have “Formal language accompanies mathematics as the weather-map accompanies the atmospheric processes” instead (Brouwer 1975: 451), but that translation was based on the book version of the so-called signific dialogues (Brouwer et al. 1939), not on the original publication in the journal Synthese (Brouwer et al. 1937). The book was edited by Mannoury, but it is not clear who changed the simile. To my mind, the original is better, because a symphony is also a construction.

6. See Brouwer 1924N: 2 [van Heijenoort 1967: 336]; 1929A: 423–424 [Mancosu 1998: 49–50]; 1949C: 492; 1952B: 510–511.

7. According to Van Dalen (1999: 106–107), it is likely that Brouwer (who entered university in 1897) learned this interpretation of PEM directly or indirectly from the teacher of logic at Amsterdam University at the time, C. Bellaar-Spruyt (1842–1901), who gave as example:

If you deny that Alexander was a great man, well, then you have to acknowledge that he was not a great man. Both opposite judgements, A. was a great man and A. was not a great man, cannot both be false.

8. Strictly speaking, Brouwer there considers not correctness and absurdity of propositions as such but of properties of a mathematical system; later (1949C: 1245; 1981A: 12), he gives the argument directly in terms of what he there calls “assertions”. But for example Wavre (1926) already adopted this direct reading, as did Heyting (1930C).

9. Brouwer’s actual theorem is about spreads, which are constructed from trees over natural numbers and in certain cases reduce to them. Also, a condition not mentioned by Brouwer is that the bar be decidable. This condition is implicitly fulfilled in the context in which the proofs of 1924 and 1927 are presented, because there the bar is defined by application of the weak continuity principle for choice sequences. This is not the case in the presentation of 1954, which is defective. See Kleene and Vesley 1965: 87–88, and Brouwer 1981A: 102.

10. Veldman (1982) has shown that for the continuity (as distinct from the uniform continuity) of these functions, the bar theorem is not needed. Continuity of course suffices for Brouwer’s strong counterexample.

11. Dummett (2000: 32) emphasizes that the conviction that there will always be open problems does not suffice to turn weak counterexamples constructed by the oscillatory number technique into strong ones. For that conviction is, he says, itself not a theorem or even a mathematical proposition.

12., the infinite form \(\forall x\in \mathbf{R}(P(x) \vee \neg P(x))\) is contradictory for certain P; but that is, as Brouwer remarks, not relevant to the project of devising finitary consistency proofs (Brouwer 1928A2: 378 [Mancosu 1998: 43]).

13. For a similar report by Freudenthal, see van Dalen 2001a: 359.

14. Brouwer, Notebook VIII, 44. Brouwer Archive, Noord-Hollands Archief, Haarlem; translation mine.

15. “Er hat die Sachen überhaupt nicht gelesen”, Bernays in an interview by Dirk van Dalen, 1977.

16. In a historical account that would emphasize the influence of ideas rather than their development, someone who would be given more attention to than is done here is Rolin Wavre (Hesseling 2003; Mancosu 1998). In the West, a prelude to systematical work on the formalization of intuitionistic logic was his paper “Logique formelle et logique empiriste” (Wavre 1926). Besides discussing differences between the classical and intuitionistic conceptions of logic, it gives a list of some propositional principles that are intuitionistically valid, as well as a list of some propositional principles that are classically valid but not intuitionistically. In this sense, it may be seen as an expanded version of Brouwer 1908C, which the otherwise well-informed Wavre however does not seem to have known. (Although the paper does not contain references, these are included in Wavre’s earlier paper of 1924, to which he refers in footnote 1. The “Bibliographie” there mentions a number of papers that appeared between 1901 and 1924 by Brouwer (including his dissertation in Dutch), Weyl, Hilbert, and Bernays.) Wavre’s 1926 paper, which was mainly expository and general in character, in effect served more to emphasize to a philosophical audience the urgency of systematic comparison than to develop one. Indeed, it sparked the Barzin-Errera episode (Hesseling 2003; Mancosu 1998). But it stopped short of presenting formalizations of either intuitionistic or classical logic. Kolmogorov published his formalization before Wavre’s paper, and Heyting’s paper from 1930 doesn’t mention it. Heyting surely knew Wavre’s 1924 paper, which he cites in his dissertation (Heyting 1925: 93); the 1926 paper was published in the same journal. There may well have been an indirect influence from Wavre on Heyting if the article played a role when Mannoury wrote his proposal for the 1927 prize question that would be successfully answered by Heyting; but that is only speculation.

17. The letter to Brouwer that Bernays mentions here seems to be lost: neither in the Brouwer Archive in Utrecht (now at the Noord-Hollands Archief, Haarlem), nor in the Bernays papers at the ETH in Zürich the letter, a draft, or a carbon copy is to be found. I am thankful to Dirk van Dalen and Eckhart Menzler-Trott for verifying this for me.

18. Letter Mannoury to Brouwer of January 26, 1927; Brouwer Archive, Noord-Hollands Archief, Haarlem.

19. By tradition, the contest was anonymous, and a motto was required to identify the winner. Heyting’s motto is from the Bible, see Matthew 7:9 and (in many but not all translations) Luke 11:11.

20. The members of the jury were, besides Mannoury, F. Schuh (professor of mathematics and mechanics in Delft) and J. Wolff (professor of mathematics at Utrecht university); like Brouwer, they had been students of Korteweg, and they had defended their theses around the same time as Brouwer, in 1905 and 1907, respectively.

21. Brouwer to Heyting, July 17, 1928; Brouwer Archive, Noord-Hollands Archief, Haarlem. Translation from the Dutch mine.

22. 1897–1940; his PhD adviser at Moscow State University was Lusin, who had worked on effective set theory, and who there had also advised Alexandrov and Urysohn (topologists who had become close friends of Brouwer’s), Khinchin (who had organized a seminar on intuitionism in Moscow in 1926), and Kolmogorov (who had published on intuitionistic logic in 1925). In such an environment, it is not surprising that Glivenko became acquainted with and interested in Brouwer’s intuitionism.

23. That way of justifying Ex Falso was already known in the 13th century.

24. In relevant logics it is objectionable as well, and this is no coincidence. See van Atten 2009.

25. In the 1950s, the formalization of intuitionistic analysis was taken up again by Kleene, which led to the influential monograph Kleene and Vesley 1965; his system was not inspired by Heyting’s, see Kleene 1973. Later attempts are Myhill 1966 and Vesley 1980.

26. As Göran Sundholm emphasized in conversation, the “relative completeness” that Heyting mentions, i.e., the richness of the presentation of logic in Principia Mathematica, must have been his reason for not taking Hilbert 1923 as his point of departure.

27. The classical system was that of Whitehead 1906, where the axioms are taken from Pieri 1898.

28. The Heyting papers are kept at the Noord-Hollands Archief, Haarlem.

29. No manuscript of such a note seems to have survived.

30. In his letter, Becker does not give the exact date. The Becker-Heyting correspondence, to the extent to which it seems to have been preserved, is kept with the Heyting papers at the Noord-Hollands Archief, Haarlem; it has been published in van Atten 2005.

31. In a letter to Heyting of May 16, 1933, Gödel says he had found the translation in June 1932 (Gödel 2003a: 71). In an earlier letter to Heyting, dated November 15, 1932 and concerning their projected joint book, Gödel asked Heyting to

say something about the relation of Hilbert’s finitism (as he advocated it in his earlier works) and intuitionism. The former might perhaps recognize even fewer inference rules and concept formations than the latter. (Gödel 2003a: 63)

Note that Gödel did not take this earlier opportunity to announce his translation to Heyting.

32. A translation of intuitionistic propositional logic into a modal logic (anticipating \(\mathbf{S4})\) had been given before Gödel, and before the earlier (failed) attempt Becker 1930 (cited by Gödel), by the Russian logician I.E. Orlov. See Došen 1992 and Bazhanov 2003. It seems that Gödel and Becker were unaware of this precursor.

33. One has the impression that Gödel (1933f: 39n.1 [1986: 301n.1]) misses this point when he comments

Kolmogorov (1932) has given a somewhat different interpretation of the intuitionistic propositional calculus, without, to be sure, specifying a precise formalism.

34. Examples of interpretations of intuitionistic predicate logic in intuitionistically acceptable systems are Veldman 1976 and de Swart 1976, 1977. Veldman (1976: 159) is explicit that his construction does not clarify the concept “intuitionistically true sentence” but is a technical device.

35. The reference was in Carnaps’s Logische Syntax der Sprache (Johansson to Heyting, November 15, 1935.)

36. As Heyting recalls in his letter of November 5, 1935 (page 3), they had in fact met, briefly, in Zürich in 1932; see also Johansson’s letter of November 15, 1935 (page 3). The latter letter is also informative about Johansson’s intellectual background. The Heyting-Johansson correspondence as kept in Heyting’s archive ends with a postcard from Johansson of January 28, 1936. The Heyting papers are at the Noord-Hollands Archief, Haarlem.

37. “Appropriate” here translates the Dutch “doelmatig”. Other translations of that term are “suitable”, “efficient”, “practical” (Groot Woordenboek Nederlands-Engels, Utrecht: van Dale 2008). The latter two may suggest a pragmatic criterion. But that can hardly be what Heyting had in mind, given that he thought of logical theorems as highly general mathematical ones, and thus, intuitionistically, certain.

38. This emends van Atten et al. 2014: 273 and van Atten & Sundholm 2016: 36, who stated that “to the best of our knowledge, the meeting never took place”.

39. The term “Katalogisierung” in this context is sometimes translated as “cataloguing” and more often as “locating”; the former seems to fit better here. Freudenthal’s definition is in fact proposed as an alternative to one that Brouwer made in a topological context (Brouwer 1926B2: 855). Freudenthal (1937a: 110) proves that the two definitions are equivalent.

40. A technical mistake in Heyting’s manuscript had been corrected by Brouwer. See van Dalen 2011: 393 for the letter, and also the extract and related remarks in Brouwer 1942A.

41. Also in later publications, e.g.,

If mathematics consists of mental constructions, then every mathematical theorem is the expression of a result of a successful construction. The proof of the theorem consists in this construction itself, and the steps of the proof are the same as the steps of the mathematical construction. (Heyting 1958C: 107)

42. In 1947 Paulette Destouches-Février proposed a middle position between Griss’ logic, which she found too extreme, and that of Brouwer and Heyting by adding to the former the definition of \(\neg p\) as \(p \rightarrow(1=2)\), but no axioms for it (Destouches-Février 1947b: 1243). However, she does not motivate this philosophically. Destouches-Février (1914–2013) published (among many other things) a number of short technical notes on intuitionistic logic, Griss’ logic, and Johansson’s logic (1945a,b, 1947a,b, 1948, 1949, 1951). She was also the French translator of Heyting’s manuscript for Heyting 1955.

43. Brouwer presented Griss 1944, 1946, 1950, 1951a, and 1951b; Heyting presented Griss 1951c and 1951d, which dealt with intuitionistic axiomatic geometry.

44. Brouwer himself has published mathematical papers that he, without mentioning it at the time, did not sanction philosophically, namely, his papers in classical topology from the period 1909–1913, in which he used the classical reasoning that philosophically he had already rejected in Brouwer 1908C. Looking back on that period, Brouwer once called those papers “free of philosophy” (philosophiefrei; Brouwer 1919D: 204).

45. Heyting (1958C: 111) remarks that “from the intuitionistic point of view this restriction is difficult to account for”, and seems to overlook that Van Dantzig addresses the classical mathematician (van Dantzig 1947b: 1092).

46. Another development by Van Dantzig was ‘stable mathematics’ (1947a, 1951), an ecumenical attempt, inspired by Gödel’s double negation translation of classical into intuitionistic arithmetic (see section 4.5.1), to develop a fragment of classical mathematics in which all theorems are equivalent to their double negations also by intuitionistic standards. Gilmore (1956) pointed out in his review of van Dantzig 1951 that the greater problem for that project is not the occurrence in classical mathematics of the principle of the excluded middle but of impredicative definitions (see on this point also Gödel *1933o and *1941).