1. See also Sundholm 2004 and Sato 1997.
2. The locus classicus here is Tarski 1953. A recent treatment of formalized interpretability is Joosten 2004.
3. 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.
4. 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.
5. 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)/(Brouwer 1975, 61n.2).
6. See Brouwer 1924N (p.2)/van Heijenoort 1967 (p.336); Brouwer 1929A (pp.423–424)/Mancosu 1998 (pp.49–50); Brouwer 1949C (p.492); Brouwer 1952B (pp.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 propositions (which he there, somewhat unfortunately, calls “assertions”). But for example Wavre (1926) already adopted this direct reading, as did Heyting (1930C).
9. Actually, a condition not mentioned by Brouwer is that the bar be decidable. This condition is implicitly fulfilled in the context in which the proofs from 1924 and 1927 are presented, but not in that of 1954. The latter is therefore defective. See Kleene and Vesley 1965 (pp.87–88) and Brouwer 1981A (p.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 (2000a, 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. As we saw in section 3.3, the infinite form ∀x∈R(P(x) ∨ ¬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 (p.359).
14. Brouwer, Notebook VIII, 44. Brouwer Archive, Utrecht; translation from the Dutch 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 1908, which the otherwise well-informed Wavre however does not seem to have known. (Although the paper does not contain a list of references, implicitly these are included in the list given in Wavre's earlier paper from 1924, to which the one from 1926 is a sequel. That list 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 contribute to answering it. 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 refers to 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, 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, Utrecht.
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 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, Utrecht. Translation from the Dutch mine.
22. 1897–1940; his PhD advisor 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. This 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 2008.
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 1968 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 Rijksarchief Noord-Holland in Haarlem.
29. In a letter to Heyting of May 16, 1933, Gödel says he had found the translation in June 1932 (Godel 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” (Godel 2003a, 63). Note that Gödel did not take this earlier opportunity to announce his translation to Heyting.
30. A translation of intuitionistic propositional logic into a modal logic (anticipating 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.
31. 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”.
32. Examples of interpretations of intuitionistic predicate logic in intuitionistically acceptable systems are Veldman 1976, de Swart 1976, and de Swart 1977. Veldman (p.159) is explicit that his construction does not clarify the concept “intuitionistically true sentence” but is a technical device.
33. No manuscript of such a note seems to have survived.
34. 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 Rijksarchief Noord-Holland in Haarlem, and has been published in van Atten 2005.