1. Introduction
Brouwer’s intuitionistic program was an intriguing attempt to reform the foundations of mathematics and was probably the most controversial one within the contours of the foundational debate of the 1920s. As a whole, Brouwer’s intuitionism did not prevail, but parts of the intuitionistic enterprise were developed over the years, and several mathematicians dedicated their efforts to presenting their own intuitionistic interpretations of Brouwer’s work. Two of the most notable attempts are those of Hermann Weyl, whose 1921 paper brought Brouwer’s intuitionism to the fore, and Arend Heyting, whose formalization of intuitionism made Brouwer’s ideas more approachable to traditional mathematicians.
The mathematical community’s reaction to Weyl’s and Heyting’s intuitionistic works was far more sympathetic than its reaction to Brouwer’s original program. Most explanations for the community’s more positive attitude toward Weyl and Heyting concern their consenting attitudes toward formal methods (van Atten Reference van Atten and Zalta2017; van Dalen Reference van Dalen1995; Hesseling Reference Hesseling2003) or their abandonment of Brouwer’s mystical-philosophical lines of thought (Franchella Reference Franchella1995; Placek Reference Placek1999; van Stigt Reference van Stigt1990; Troelstra Reference Troelstra1991). According to Dennis Hesseling, Weyl’s clear and coherent writing style (as opposed to Brouwer’s overly technical style) made his 1921 paper considerably more approachable to the classical mathematicians, who often found Brouwer’s papers incomprehensible (Hesseling Reference Hesseling2003, 61–62). Weyl’s use of metaphors, and especially his use of the terms crisis and revolution, also played a role in attracting readers’ attention. Hesseling claims:
It is impossible to say if Weyl had any specific revolution in mind when he wrote these lines. However, one can try to re-create the impression these words may have had on readers in 1921. What did it mean to them to read an important mathematician proclaim the “revolution”? They could have been reminded of the German 1918 revolution, by which the republic had been declared. If this was the case, it means that they saw Weyl’s intuitionism as linked to republican, democratic Germany. By 1921, however, the German revolution was generally considered “stolen,” and the most likely revolution was a communist one. … Thus, Weyl’s call could be seen as much more radical. (Hesseling Reference Hesseling2003, 303–4)
Historian of science Paul Forman argued that Weyl’s rhetoric was shaped by the “social-intellectual atmosphere in the aftermath of Germany’s defeat” (Forman Reference Forman1971, 61). He claimed that both Weyl and Hilbert “at the very least saw close parallels between the crisis in mathematics and the political crises then wracking Germany,” and he maintained that Germany’s defeat was the main reason behind the German mathematical community’s increasing interest in Brouwer’s intuitionism during the 1920s (Forman Reference Forman1971, 60–61). This argument is part of Forman’s broader approach, known as the Forman thesis, in which he put forward the argument that the cultural values prevalent in a given place and time could affect the very content of scientific knowledge. According to Forman’s thesis, the culture of Weimar Germany influenced the way many scientists, including Hermann Weyl, interpreted the concept of causality in physics and quantum mechanics (Forman Reference Forman1971; Norris Reference Norris2000). Forman’s thesis raised an intense and controversial debate among historians and physicists that has remained at the heart of discussions about the historical relationship between science and culture ever since (Carson et al. Reference Carson, Kojevnikov, Trischler, Carson, Kojevnikov and Trischler2011; Kraft and Kroes Reference Kraft and Kroes1984).
The popularity of Heyting’s brand of intuitionism is also often attributed to its disentanglement from Brouwer’s philosophical considerations. Philosopher Miriam Franchella points out that “Arend Heyting is well known not only for his own contributions to intuitionism, but also for his expository efforts to make Brouwer’s ideas more accessible and more widely known … by separating its mystic philosophy (seen as bizarre) from its basic concepts for mathematics” (Franchella Reference Franchella1995, 105). In a similar vein, philosopher Thomas Placek notes that “an undeniable advantage of Heyting’s approach is that it puts the fate of intuitionism on a more ‘down-to-earth’ ground” (Placek Reference Placek1999, 106), in the sense that Heyting’s intuitionism was based on considerations that were perceived as less philosophical or bizarre than Brouwer’s.
Yet such explanations portray only part of the picture because they mostly account for the practical differences between the three stories. In the current article, I argue that the differences between the intuitionistic versions of Brouwer, Weyl, and Heyting run deeper. The three mathematicians held different views regarding the normative boundaries of the discipline that were reflected in the respective versions of intuitionism each produced. The following pages are devoted to a careful examination of each approach and the impact of the differences on the community’s respective responses.
The article proceeds by analyzing the changes suggested by Brouwer, Weyl, and Heyting in terms of changes to the practical layer of mathematics, on the one hand, and changes to the normative layer of mathematics, on the other. Such an analysis takes into account how each conceived the way mathematics should be properly done and how this manifested in their respective work. This characterization provides a richer account of each story and draws a possible connection between the community’s reaction and the scope of change each mathematician suggested.
2. Mathematics’ two (three?) layers
In his article “Linearity and Reflexivity in the Growth of Mathematical Knowledge” (1989), historian Leo Corry presents a theory of how mathematical knowledge progresses and how developments in mathematics take place. He describes mathematics as comprised of two different layers of thought: the body of knowledge, which refers to theorems, proofs, techniques, and results obtained within mathematics, and the image of knowledge, which covers the normative aspects of the discipline. The firm distinction between “image” and “body of knowledge” was first proposed by Yehuda Elkana (Reference Elkana1978, Reference Elkana, Mendelson and Elkana1981); Corry borrows it and applies it, with an important twist, to mathematics.
Elkana suggested that every scientific discipline can be viewed as comprising two interconnected layers of thought: the body of knowledge and the image of knowledge. Elkana characterizes the “body of knowledge” as where the research is done; it consists of various first-order scientific theories, concepts, and procedures (Elkana Reference Elkana1978, 315). Second-order “images of knowledge,” by contrast, govern certain aspects of scientific activity that determine but are not contained within the body of knowledge, such as the sources of knowledge, the legitimization of knowledge, the audience of knowledge, and relatedness to prevailing norms and ideologies. The distinction between the two lies in the questions they address:
[I]n the process of scientific activity, the most important decisions involve problems of choice: the decision as to whether an experiment or a calculation is satisfactory, clear enough, reliable or to be discarded; … All these decisions are not reached on the basis of the body of knowledge—that is, on the discipline itself, in which the research is being done. The body of knowledge—let us say physics or biology—does not give us clues as to what is beautiful, interesting, feasible, frontier-of knowledge, convincing, broad or narrow, worthwhile, in good taste, thematically on the right track, too risky, premature, repetitive, and so on—yet these are the very terms in which problem-choice and scientific decisions are couched. (Elkana Reference Elkana1978, 315)
Accordingly, science progresses in the course of addressing two different types of questions: those concerned with the tools and methods employed in making a discovery or forming a new theory and those to do with the guiding principles and normative boundaries of the discipline itself.
Applying Elkana’s distinction to mathematics, Corry distinguishes between the body of mathematical knowledge, which includes theories, facts, methods, and open problems, and the image of mathematics, which includes guiding principles that help us discuss questions that arise from the body of mathematical knowledge but cannot be settled within it. The distinction between the two domains, claims Corry, is “by its very definition, somewhat blurred and always historically conditioned” (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001, 168), but he does not suggest that one layer is more important to the development of mathematics than the other.
Corry perceives the body and image of knowledge as organically interconnected domains in the history of a discipline, but he does not regard their relationship as cause and effect (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001, 177). Hence, transitions between images of knowledge are unique processes and distinct from transitions in the body of knowledge. Philosopher Lukas Verburgt calls into question Corry’s distinction between the “body” and “image” of mathematics and argues that it should be amended to accommodate the reciprocal dynamics of a science’s image and body of knowledge (Verburgt Reference Verburgt2015). Verburgt’s central argument is that transitions in the domain of mathematics cannot be conceived of as transformations of one “image” into another “image” of the same “body” of knowledge and, in his leading example concerning the birth of modern probability theory, Verburgt shows how transformations between images of knowledge destroyed concepts in the body of knowledge (Verburgt Reference Verburgt2015, 11–20). The current article shows how the retelling of Brouwer’s, Weyl’s, and Heyting’s stories in light of Corry’s model raises some interesting questions regarding the direction of changes in the body and image of knowledge and whether changes in the image of mathematics can occur independently of changes in the body of mathematics. Although it is beyond the scope of this article to provide a comprehensive answer to these intriguing questions, it should be noted that Corry maintains that there is not only one direction in which mathematical transitions can occur (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001). As a case study, Corry examines the structural image of a specific mathematical discipline, namely, algebra, by analyzing van der Waerden’s Moderne Algebra, which presents the body of algebraic knowledge as deriving from a single unified perspective and in which all the relevant results in the field are achieved using similar concepts and methods (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001, 172).Footnote 1 The systematic study of different varieties of algebra through a common approach is what Corry calls a structural image of algebra. Although the transition to a new structural image in the case of van der Waerden’s Moderne Algebra was enabled due to changes in the body of knowledge, it does not imply that this is mandatory (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001, 177).
Similar to Elkana, Corry identifies the difference between the two layers in the range of questions they address: the body of knowledge answers questions dealing with the subject matter of mathematics, and the image of knowledge addresses questions concerning mathematicians’ cognitive and normative views, such as the following:
-
Which of the open problems of the discipline most urgently demands attention?
-
What is to be considered a relevant experiment or a relevant argument?
-
What procedures, individuals, or institutions have the authority to adjudicate disagreements within the discipline?
-
What is to be taken as the legitimate methodology of the discipline?
-
What is the most efficient and illuminating technique that should be used to solve a certain kind of problem in the discipline? (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001, 168)
Corry’s novel claim is that unlike in other disciplines, in mathematics, questions pertaining to both the body and image of knowledge are contained within mathematics itself. Mathematics is uniquely endowed with an ability to “absorb certain images of knowledge directly into the body of knowledge” (Corry Reference Corry, Bottazzini and Dahan-Dalmédico2001, 3). In every other discipline, there is a constant interaction between the body and image of knowledge; in mathematics, however, there is a special interconnection between the two layers:
Only in mathematics there is an intermediate layer, reflexive knowledge; in no other instance may claims about a given discipline qua discipline be inspected with the same methodological tools and through the same criteria as any other claim of that discipline and, accordingly, be included in the body of knowledge or rejected from it. (Corry Reference Corry1989, 415)
This reflexive aspect of mathematics enables it to examine the nature of the discipline itself by exploring the same two-tiered framework that is used in everyday methodological practice. Some mathematical theories can be classified easily into one of the two tiers, whereas other mathematical theories may encompass an aspect of both. Consider proof theory as an example of reflexive knowledge. Mathematics is the only discipline that has a dedicated doctrine that, on the one hand, examines how its methods should be properly done and, on the other hand, represents proofs as formal mathematical objects and analyzes them through mathematical techniques.
The current article proposes viewing Heyting’s formalization of intuitionism as part of this intermediate layer of mathematics because it absorbed an intuitionistic image of knowledge into the classical body of knowledge by using formal methods to express intuitionistic ideas. This argument will be further elaborated and discussed in sections 5 and 6. But first, let us set the scene by exploring how each of the three mathematicians envisaged the normative boundaries of the discipline in terms of the image and body of mathematical knowledge, as well as which layers their intuitionistic program aimed to change.
3. Brouwer on the image and body of knowledge
Brouwer’s views on which questions belong to the body and which to the image of mathematical knowledge can be extracted from his views regarding the difference between intuitionism and formalism:
The question where mathematical exactness does exist, is answered differently by the two sides; the intuitionist says: in the human intellect, the formalist says: on paper. … For the formalist therefore mathematical exactness consists merely in the method of developing the series of relations, and is independent of the significance one might want to give to the relations or the entities which they relate. And for the consistent formalist these meaningless series of relations to which mathematics are reduced have mathematical existence only when they have been represented in spoken or written language together with the mathematical-logical laws upon which their development depends, thus forming what is called symbolic logic. (Brouwer Reference Brouwer and Heyting1912, 83)
As Brouwer saw it, the intuitionist and the formalist perceive the normative boundaries of mathematics differently. The intuitionist perceives mathematical objects as creations of the mind, not as mere symbols and formulas written on paper. Moreover, to the intuitionist, the meaning of mathematical relations cannot be detached from the symbols that represent them. Mathematical exactness cannot be based only on axioms and formulas:
The viewpoint of the formalist must lead to the conviction that if other symbolic formulas should be substituted for the ones that now represent the fundamental mathematical relations and the mathematical-logical laws, the absence of the sensation of delight, called “consciousness of legitimacy,” which might be the result of such substitution would not in the least invalidate its mathematical exactness. (Brouwer Reference Brouwer and Heyting1912, 84)
According to Brouwer, questions concerning the nature and origins of mathematical objects are certainly part of the image of mathematical knowledge. However, not every meta-mathematical question should be pursued within the discipline. Some meta-mathematical considerations are not part of the image of mathematical knowledge:
To the philosopher or to the anthropologist, but not to the mathematician, belongs the task of investigating why certain systems of symbolic logic rather than others may be effectively projected upon nature. Not to the mathematician, but to the psychologist, belongs the task of explaining why we believe in certain systems of symbolic logic and not in others, in particular why we are averse to the so-called contradictory systems in which the negative as well as the positive of certain propositions are valid. (Brouwer Reference Brouwer and Heyting1912, 84)
Brouwer’s intuitionism holds that the existence of a mathematical object is equivalent to the possibility of its construction in one’s mind. Here arises an important philosophical distinction between, on the one hand, objects like finite numbers and a constructive countable set, which are objects that we finite beings can intuitively grasp, and on the other hand, the Cantorian collection of all real numbers, which is an infinite entity that exceeds our grasp. Brouwer regarded the former entities as “finished” or “finish-able,” whereas the latter is “unfinished.” A “finished” set is produced by a recognizable process (i.e., a process that one can construct), yielding some legitimate grasp of the object with all its parts (i.e., that the parts are “determined” by the initial grasp). An “unfinished” collection is one that we cannot grasp in a way that suffices to determine all its parts (Brouwer Reference Brouwer and Heyting1952; Posy Reference Posy, van Atten, Boldini, Bourdeau and Heinzmann2008).
Brouwer used this distinction to confront Cantor’s perception of infinity.Footnote 2 Brouwer accepted ω-sequences as legitimate mathematical objects because they are sequences of discrete elements generated by a countably ordered process:
This intuition of two-oneness, the basal intuition of mathematics, creates not only the numbers one and two, but also all finite ordinal numbers, inasmuch as one of the elements of the two-oneness may be thought of as a new two-oneness, which process may be repeated indefinitely; this gives rise to the smallest infinite ordinal ω. (Brouwer Reference Brouwer and Heyting1912, 85–86)
However, they are the only infinite objects he accepted:
In chapter 1 we have seen that there exist no other sets than finite and denumerably infinite sets and continua; this has been shown on the basis of the intuitively clear fact that in mathematics we can create only finite sequences, further by means of the clearly conceived “and so on” the order type ω. (Brouwer Reference Brouwer1907, 142–43)
Brouwer addressed the set of real numbers negatively as “denumerably unfinished,” pointing out that given a denumerable subset, we can straightaway find an element of the continuum that is not in the given subset, but there is no positive existence claim to support the existence of such element. Hence, he proclaimed Cantor’s second number class and any ranked order of increasing cardinalities as illegitimate mathematical objects, mere “expression[s] for a known intention” (Brouwer Reference Brouwer1907, 148).
The alternative Brouwer suggested to the Cantorian hierarchy consisted of only finite cardinalities:
Thus, we distinguish for sets the following cardinal numbers, in order of magnitude:
-
1. the various finite numbers.
-
2. the denumerably infinite.
-
3. the denumerably unfinished.
-
4. the continuous. (Brouwer Reference Brouwer1907, 149)
Here, the term denumerably unfinished refers to a set of which only a denumerable subset is well defined, and new objects belonging to the set can always be added using a fixed procedure (Brouwer Reference Brouwer1907, 187–88).Footnote 3 As for the intuition of the continuum itself, Brouwer firmly believed that we have an intuitive grasp of the continuum as a whole:
Having recognized that the intuition of “fluidity” is as primitive as that of several things conceived as forming a unit together, the latter being at the basis of every mathematical construction, we are able to state properties of the continuum as a “matrix of points to be thought of as a whole.” (Brouwer Reference Brouwer1907, 8–9)
However, the continuum as a whole was given to us by intuition; a construction for it, an action that would create from the mathematical intuition “all” its points as individuals, is inconceivable and impossible. (Brouwer Reference Brouwer1907, 62)
Thus, a continuum that is constructed out of a set of independently given points (like the Cantorian continuum) cannot be considered a legitimate mathematical entity. No set of points can exhaust the continuum because, in Brouwer’s view, it is a unity in its own right (Brouwer Reference Brouwer1907; Posy Reference Posy and Shapiro2005).
According to the Brouwerian image of mathematical knowledge, the principle of excluded middle is also deemed unacceptable. In “The Unreliability of Logical Principles” (Brouwer Reference Brouwer and Heyting1908), Brouwer explained the problematic aspects of accepting the principle of excluded middle as valid in both finite and infinite sets:
As long as only certain finite discrete systems are posited, the investigation into the possibility or impossibility of a fitting can always be terminated and leads to an answer, whence the principium tertii exclusi is a reliable principle of reasoning. That also infinite systems, with respect to so many properties, are controlled by finite means, is achieved by surveying the denumerably infinite sequence of the whole numbers by complete induction, namely by observing properties, that is, fittings, that hold for an arbitrary whole number, and in particular also contradictions, that is, impossible fittings, that hold for an arbitrary whole number. However, that from the systems posited in a question, one can be derived that reads the question by means of a complete induction, on the basis of an invariant in a denumerably infinite sequence, and thereby solves it, is found only a posteriori, when accidentally the construction of such a system has succeeded. For the whole of the systems that can be developed from the question posed is denumerably unfinished, whence cannot be a priori investigated methodically regarding the presence or absence of a system that decides the question. And it is not excluded, that by a draw as lucky as the ones that have so often led to a decision, we will one day see from the denumerably infinite system of possible developments that it is unsolvable. So that in infinite systems the principium tertii exclusi is as yet not reliable. (Brouwer Reference Brouwer and Heyting1908, 108)
The principle of excluded middle can only be used as a reliable tool in finite systems where each object of the set can be examined (in principle) by means of a finite process. Within a finite system, one can eventually determine whether there is a member of the set with the property A or that every member of the set lacks the property A. However, in infinite systems, it is not possible to examine every object of the set (not even in principle); thus, even if one never finds a member of the set with the property A, it does not prove that every member of the set lacks the property A (Brouwer Reference Brouwer and Heyting1908, Reference Brouwer1918).
Brouwer believed that Peano, Russell, Cantor, and Bernstein had overlooked the essential role that the human intuition of mathematics plays when moving from investigating finite sets to infinite sets. In finite sets, the examination of each object of the set can be conducted by a machine or a trained animal. However, with regard to infinite domains, human intuition becomes indispensable, and the mathematician can no longer rely solely on logical rules or “linguistic buildings,” to use Brouwer’s phrasing (Brouwer Reference Brouwer and Heyting1908).
Together with the restricting concept of infinity and his demand that mathematical objects must be constructed, Brouwer introduced a new image of mathematical knowledge, which he considered as the only proper way to do mathematics. In doing so, the idea of mathematical truth and its relation to the provability and refutability of a mathematical statement was redefined: in the newly proposed intuitionistic theory, knowing that a statement P is true means having proof of it; to negate P is to claim that P is refutable (i.e., that a counterexample exists), but it does not imply that “not P” is provable (Brouwer Reference Brouwer and Heyting1912; Heyting Reference Heyting1956; Sundholm and van Atten Reference Sundholm, van Atten, van Atten, Boldini, Bourdeau and Heinzmann2008). One of the many implications of such a thorough reformation was to render proofs of mathematical existence by contradiction an illegitimate technique within the discipline.
Although Brouwer’s early work (until 1918) showed that some mathematical statements do not hold intuitionistically, and vice versa, it was only when he introduced choice sequences that it became apparent that intuitionism is incomparable with classical mathematics (Iemhoff Reference Iemhoff and Zalta2008). According to intuitionism, there is only potential infinity, which means that infinite objects can only be produced by a process that generates them one by one. A choice sequence is an infinite sequence of numbers, elements, or finite objects, created by the “free will” of the “creating subject” (Brouwer Reference Brouwer and Heyting1949; Niekus Reference Niekus2005). There are “lawlike” and “lawless” sequences; a lawlike sequence is a sequence that can be determined by a law or an algorithm, whereas a lawless sequence is not subject to any law (Fourman Reference Fourman, Troelstra and van Dalen1982; Dummett Reference Dummett1977). The natural numbers are an example of a lawlike sequence, and the sequence of casts of a die can represent a lawless sequence in the sense that “at any stage only finitely results are known, but we cannot say anything about future values” (Troelstra Reference Troelstra1977, 12; for a detailed examination of lawlike and lawless sequences, see also Kreisel [Reference Kreisel1968]).
From 1918 onward, Brouwer spoke of choice sequences as a fundamental part of his intuitionistic mathematics, which allowed him to describe the intuitionistic continuum with continuity axioms (Brouwer Reference Brouwer and Heyting1948, Reference Brouwer and Heyting1952). However, the use of the continuity axioms entailed far-reaching implications for the classical body of mathematical knowledge because classically invalid statements can derive from axioms such as the weak continuity axiom and the full axiom of continuity (van Atten and van Dalen Reference van Atten and van Dalen2002).Footnote 4
Brouwer’s intuitionistic program entailed deep and comprehensive changes to the image of knowledge, yet it did not call into question a single theory in the body of classical mathematics. No previously proven results were rejected; some were deemed unacceptable according to the new Brouwerian image of knowledge, but none were proven wrong or contradictory in consequence of Brouwer’s intuitionism. Moreover, Brouwer did not use any methods from the body of knowledge to express his intuitionistic ideas. The changes Brouwer suggested affected only the image of mathematical knowledge. Nonetheless, Brouwer’s ideas drew the attention of Hermann Weyl, physicist and mathematician, who was searching to find a solution to the same problem that occupied Brouwer.
Before discussing Weyl’s version of intuitionism, a word of clarification is in order. The versions of intuitionism suggested by Brouwer (and Weyl, as demonstrated in the next section) proposed changes to the body of mathematical knowledge that conflicted with classical reasoning, but these changes did not disprove mathematical theories. Both Brouwer and Weyl were extremely troubled by the problematic and unstable foundations of mathematics. Each suggested a somewhat different alternative to classical mathematics, which derived from the basic assumptions that mathematics is a creation of the mind and that the only legitimate mathematical objects are those obtained by construction. Hence, from their intuitionistic point of view, some classical theories were “rejected” or not valid based on being nonconstructive. However, to a nonintuitionistic mathematician, who is relatively indifferent to the paradoxes of Cantor’s set theory and does not view mathematics as a mental construction, there is no (classical) logical reason to reject or invalidate any working theory. Thus the “rejected” or “unacceptable” classical theories were not rejected based on logical fallacies or mistakes but on fundamental philosophical-normative disagreements.
4. Hermann Weyl on the image and body of mathematical knowledge
In the early stages of the history of intuitionism, Hermann Weyl was among the few mathematicians who, at some point, embraced Brouwer’s intuitionism. Weyl displayed a keen interest in philosophy, specifically in idealism and phenomenology (Feferman Reference Feferman1998; Scholz Reference Scholz, Hendricks, Pedersen and Jørgensen2000). The emergence of the paradoxes of set theory at the turn of the century intensified the sense among mathematicians that something was fundamentally wrong with the foundations of mathematics. Deeply disturbed by their possible ramifications, Weyl embarked on a journey to search for an alternative to Cantor’s set-theoretic approach. Das Kontinuum (Weyl Reference Weyl1918) was his part-constructive response to the turmoil. According to Dirk van Dalen, the solution Weyl suggested was not a “mere technicality for escaping unpleasant phenomena; it was based on the philosophical insights of phenomenology. Phenomenology was his explicit point of departure” (van Dalen Reference van Dalen2013, 309).
It is worth pointing out that there is, in fact, an extensive discussion about how Weyl’s philosophical leanings shaped his foundational position in the debate between intuitionism, constructivism, and formalism-finitism in the 1920s. Solomon Feferman argued that Weyl’s criticism of the set-theoretical approach led him to embrace a predicativist position in Das Kontinuum (Weyl Reference Weyl1918; see Feferman [Reference Feferman1988] for further discussion). Erhard Scholz describes Weyl’s inclination toward intuitionism as rooted in philosophical considerations deeply influenced by Fichte’s approach to the concept of continuum and space (Scholz Reference Scholz, Hendricks, Pedersen and Jørgensen2000), whereas Norman Sieroka claims that during the 1920s, Husserl’s phenomenology motivated Weyl to adopt Brouwer’s intuitionism, and Fichte’s constructivism motivated him to adopt formalism—which explains why, after his brief affiliation with Husserl’s “intuitionistic-phenomenological” approach, from Reference Brouwer1925 Weyl’s foundational views drifted toward Fichte’s “formalistic-constructivist” approach (Sieroka Reference Sieroka2009, Reference Sieroka, Bernard and Lobo2019).
Be that as it may, in 1921, Weyl published a paper entitled “On the New Foundational Crisis in Mathematics” (Weyl Reference Weyl and Mancosu1921) that was not only a clear exposé of Brouwer’s intuitionistic ideas (van Dalen Reference van Dalen2013; Hesseling Reference Hesseling2003) but also an introduction to Weyl’s own intuitionistic approach. The paper begins with a brief description of the problem at hand, namely, the antinomies of set theory and its “vicious circle,” followed by an introduction to Weyl’s earlier attempt in Das Kontinuum to establish a solid foundation for analysis, which he had abandoned in favor of Brouwer’s theory (Weyl Reference Weyl and Mancosu1921, 86). Throughout the second section, Weyl elaborates on Brouwer’s ideas, including concepts such as sequences, laws, mathematical existence, real numbers, and continua. It is only toward the end of the article that Weyl articulates precisely how his own intuitionistic foundational theory differs from Brouwer’s intuitionism:
As far as I understand, I no longer completely concur with Brouwer in the radical conclusions drawn here. After all he immediately begins with a general theory of functions (the name “set” is used by him to refer to what I call here functio continua), he looks at properties of functions, properties of properties, etc., and applies the identity principle to them. (I am unable to find a sense for many of his statements.) From Brouwer I borrowed (1) the basis that is essential in every respect, namely, the idea of the developing sequence and the doubt in the principium tertii exclusi, and (2) the concept of the functio continua. I am responsible for the concept of the functio mixta and the conception I summarize in the following three theses: (1) The concept of a sequence alternates, according to the logical connection in which it occurs, between “law” and “choice,” that is, between “Being” and “Becoming”; (2) universal and existential theorems are not judgements in the proper sense; they do not make a claim about a state of affairs, but they are judgement instructions and judgement abstracts, respectively; (3) arithmetic and analysis merely contain general statements about numbers and freely developing sequences; there is no general theory of functions or sets of independent content. (Weyl Reference Weyl and Mancosu1921, 109–10)
Two important observations arise from this quote. The first is that the intuitionistic versions of Brouwer and Weyl are rooted in foundational assumptions that are fundamentally different from those of classical mathematics (the principle of excluded middle, the concept of the continuous continuum, and mathematical existence are three prominent examples). Hence, their intuitionistic versions render several classical proofs, concepts, and theories intuitionistically unacceptable (e.g., proofs of existence by contradiction). However, it does not imply that any classical theorem has been proved wrong or contradicted by their intuitionistic attempts. In this sense, Brouwer and Weyl presented new bodies of knowledge comprising intuitionistic theories that were incompatible with classical mathematics, but they did not engage with classical theories or proofs whatsoever. The incompatibility of their intuitionistic versions and classical mathematics derived from differences in the basic assumptions (some might argue that they are merely philosophical differences), not from disproving a theory or pointing to a logical fallacy in a classical proof.
The second significant observation is that the differences between Brouwer’s and Weyl’s versions of intuitionism are mostly differences between the intuitionistic bodies of knowledge they suggest because they apply different logical connections and mathematical definitions and address the legitimacy of certain mathematical existence statements differently. However, their philosophical points of departure, at least in 1921, are relatively similar; both held similar views regarding normative questions pertaining to how mathematics should be properly done and which general logical principles should be deemed unacceptable (e.g., the principle of excluded middle). Hence, their suggested images of knowledge are quite alike.
Brouwer’s comments on this part of Weyl’s paper indicate that both men were well aware of their differences:
[with respect to (1)] for me “emerging sequence” is neither one; one considers sequences from the stand-point of a helpless spectator, who does know at all in how far the completion has been free. … I do, however, not agree with (2) and (3). (van Dalen Reference van Dalen1995, 160)
Two additional differences between Brouwer’s and Weyl’s versions of intuitionism emerge from Weyl’s 1921 paper. The first concerns how each addressed choice sequences and their properties: whereas Brouwer allowed choice sequences given by law, Weyl excluded lawlike sequences from the domain of choice sequences (van Dalen Reference van Dalen1995, 152). For Brouwer, a choice sequence is an individual object, and he did not restrict the notion of choice in the sense that no matter how the path to creating such a sequence was chosen, it was an eligible sequence (Brouwer Reference Brouwer and Heyting1948). Weyl did not regard choice sequences as possessing the sort of individuality a lawlike sequence has:
A sequence is created by arbitrary choosing the individual numbers one by one … An individual determined sequence (and I mean determined in infinitum) can only be defined by a law. If, however, a sequence is created step by step through free acts of choice, then it must be seen as a developing one [eine werdende]. A developing choice sequence can only meaningfully be said to have properties for which the decision “yes or no” (does the sequence possess the property or not) can already be obtained when the sequence has reached a certain stage such that the further development of the sequence beyond this point of Becoming, however it may turn out, cannot reverse this decision. (Weyl Reference Weyl and Mancosu1921, 94).
Weyl focused his attention on getting the choice process right, whereas Brouwer did not elaborate on the choice process at all. In Weyl’s summary of the differences between his intuitionistic approach and Brouwer’s approach, it becomes clear that when Weyl refers to “developing” or “becoming” choice sequences, he means lawless sequences (Weyl Reference Weyl and Mancosu1921, 109–10). Brouwer’s and Weyl’s different views on choice sequences and their properties represent a difference between the intuitionistic bodies of knowledge they suggested because the definition of choice sequences and the processes to obtain them are part of the practices and theories of the discipline.
The second difference concerns the consequences of adopting an intuitionistic point of view on logic, particularly regarding existence statements. In Brouwer’s view, existence statements are legitimate as long as they can be interpreted constructively, even if they do not contain information. Weyl, on the other hand, argued that legitimate existence statements are only those that contain information, such as “Two is an even number” (as opposed to “There is an even number,” which is not a proper judgment because it does not provide us with the specific object). Nevertheless, both consent that constructive procedures are the only proper way to define existence statements, and this consensus is part of their suggested images of knowledge.
Despite their differences, Weyl and Brouwer shared similar philosophical incentives to reform the foundations of mathematics. Weyl was deeply influenced by Kant’s notion of the primacy of intuition, and he describes his own philosophical voyage as deriving from Kant’s idea that space and time are not inherent in the objects of the world (Weyl Reference Weyl, Saaty and Weyl1955). Brouwer shared a similar impression with Kant’s approach to the apriority of time and dedicated the second chapter of his dissertation to improving Kant’s view of the a priori (Brouwer Reference Brouwer1907, 99–131). During the 1910s, Weyl was attracted to idealist philosophy, specifically to the works of Husserl and Fichte, which played a significant role in his foundational thought and the development of his inclination toward constructive approaches and, later, toward Brouwer’s intuitionistic ideas (Scholz Reference Scholz2005; Sieroka Reference Sieroka2009, Reference Sieroka, Bernard and Lobo2019).
Because Weyl’s metaphysical outlook included some realistic aspects, his idealism was different from Brouwer’s idealism because Brouwer’s philosophy amounted virtually to solipsism, whereas Weyl still seemed to have cleaved to phenomenologyFootnote 5 (Mancosu and Ryckman Reference Mancosu and Ryckman2002; Bell and Korté Reference Bell, Korté and Zalta2015). However, this common philosophical ground and their shared view regarding the primary intuition of time contributed to Weyl’s leaning toward intuitionism. Both men shared similar views in 1921 regarding the legitimate methodologies and appropriate techniques that should be practiced within the discipline. For example, Brouwer and Weyl agreed that existential and universal statements are meaningful only if they are defined using constructive procedures (Weyl Reference Weyl and Mancosu1921, 89). In this sense, Weyl’s views regarding the normative boundaries of the discipline are quite similar to Brouwer’s.
Nonetheless, from Weyl’s 1921 paper emerges another significant difference between the two regarding the connection between the image and the body of knowledge. After introducing the concept of functio continua, Weyl writes:
But let me emphasize again that individual determined functions of this sort occur from case to case in theorems of mathematics, yet one never makes general theorems about them. The general formulation of these concepts is therefore only required if one gives an account of the meaning and the method of mathematics; for mathematics itself, and the content of its theorems, it does not come into consideration at all. (Weyl Reference Weyl and Mancosu1921, 106)
Brouwer, who received an early draft of Weyl’s paper, commented on this specific paragraph:
It seems to me that the whole purpose of your paper is endangered by the end of the second paragraph of page 34. After you have roused the sleeper, he will say to himself: “So the author admits that the real mathematical theorems are not affected by his considerations? Then he should no longer disturb me!” and turns away and sleeps on. Thereby you do our cause injustice, for with the existence theorem of the accumulation point of an infinite point set, many a classical existence theorem of a minimal function, as well as the existence theorems for geodesics without the second differentiability condition, loses its justification! (van Dalen Reference van Dalen1995, 149)
Brouwer, as noted earlier, saw a firm and inseparable connection between mathematical tools, formulas, and methods and the meaning or relations they represent. Weyl, on the other hand, distinguished between mathematical meaning and mathematics itself: accounts of meaning require intuitionistic definitions and concepts, but intuitionism’s fundamental considerations are somewhat less relevant for the everyday work of practicing mathematicians.
Weyl’s 1921 paper was an important milestone in the foundational debate. It certainly received more reactions than Brouwer’s papers ever did, and it created quite a stir in the mathematical community (van Dalen Reference van Dalen1995; Hesseling Reference Hesseling2003). However, most reactions to Weyl’s paper were written within the inner circle of Brouwer, Mannoury, Weyl, Fraenkel, and less frequently, Hilbert and Becker, between 1921 and 1926. According to the historical evidence Dennis Hesseling provides, the debate reached its peak between 1927 and 1933, and most reactions during this period were written in response to Heyting’s work (Hesseling Reference Hesseling2003, 96, 363–69). Why were mathematicians more engaged with Heyting’s intuitionism than with Brouwer’s or Weyl’s versions of intuitionism? What is unique to Heyting’s version of intuitionism?
Similar to Brouwer’s intuitionism, the changes suggested by Weyl’s intuitionism affected only the images of knowledge. It is true that the works of Brouwer and Weyl posed some interesting and deep questions for a small (but important) sector of the mathematical community, but they did not disprove a single theory from the classical body of knowledge, nor did they use classical methods to articulate their intuitionistic ideas. Unlike the works of Brouwer and Weyl, Heyting’s formalization of intuitionistic mathematics entailed a different kind of change to the body and image of mathematical knowledge.
5. Heyting’s intuitionism as a change to both the image and body of knowledge
Arend Heyting was Brouwer’s student at the University of Amsterdam during the 1920s. His dissertation, supervised by Brouwer, was devoted to an extensive study of axiomatization in constructive mathematics. In 1927, the Dutch Mathematical Association announced an essay competition on the formalization of Brouwer’s intuitionist theories. A year later, Heyting won the prize, and his remarkable essay was extended and published in 1930. Heyting continued to develop this line of thought into a series of papers presenting a formalization of intuitionistic logic and mathematics, and his papers started to gain attention within the foundational debate (Heyting Reference Heyting and Mancosu1930a, Reference Heyting1980). Heyting’s formalization project during the 1930s purported to combine, into one big system, intuitionistic propositional and predicate logic, arithmetic, and analysis. The parts covering logic and arithmetic, excluding the principle of excluded middle, were subsystems of their classical counterparts (Heyting Reference Heyting and Mancosu1930a, Reference Heyting1930b, Reference Heyting1930c).
Like Brouwer, Heyting believed that mathematical entities do not exist outside of the human mind:
Intuitionistic mathematics consists … in mental constructions; a mathematical theorem expresses a purely empirical fact, namely the success of a certain construction. “2 + 2 = 3 + 1” must be read as an abbreviation for the statement: “I have effected the mental constructions indicated by “2 + 2” and by “3 + 1” and I have found that they lead to the same result. (Heyting Reference Heyting1956, 8)
However, Heyting held a different view regarding the role of philosophy in mathematics:
[W]e must distinguish between the simple practice of mathematics and its valuation. In order to construct mathematical theories no philosophical preliminaries are needed, but the value we attribute to this activity will depend upon our philosophical ideas. (Heyting Reference Heyting1956, 9)
Heyting’s disentanglement from Brouwer’s philosophical considerations should be taken with a pinch of salt; Heyting may say that the “only philosophical thesis of mathematical intuitionism is that no philosophy is needed to understand mathematics” (Heyting Reference Heyting1974, 79), but even his own writings show that mathematical intuitionism depends on views and choices concerning meaning, introspection, and the limits of acceptable idealization (Heyting Reference Heyting1956, Reference Heyting1974). In this respect, Heyting was no less philosophically engaged than Brouwer. Hence, even though Heyting abandoned Brouwer’s philosophical grounding, his image of mathematical knowledge remained squarely intuitionistic. According to several Brouwer scholars and biographers, the philosophical origins of Brouwer’s intuitionistic thinking are to be located in Kant’s philosophy (van Dalen Reference van Dalen1978; van Stigt Reference van Stigt1990). Brouwer himself felt that at least part of his own philosophical view of the a priori could be traced back to Kant’s philosophy, pending some adjustments to Kant’s concept of the a priori (Brouwer Reference Brouwer1907, 99). He explicitly states that his dissertation’s principal goal is to “rectify Kant’s point of view on apriority in the experience and bring it up to date” (Brouwer Reference Brouwer1907, 114). Heyting’s intuitionistic mathematics, on the other hand, was much less rooted in Kant’s philosophy, and several of Brouwer’s most significant concepts, such as consciousness and mind, play no role in Heyting’s approach (Heyting Reference Heyting1974). Although Heyting and Brouwer may have disagreed on what is intuitively clear—as Heyting himself put it, “it has proved not to be so intuitively clear what is intuitively clear in mathematics” (Heyting Reference Heyting, Nagel, Suppes and Tarski1962, 195)—as intuitionists, they both agreed that mathematical entities do not exist outside of the human mind.
Yet, unlike his teacher, Heyting insisted on adopting a formalist methodology in practice. In an interview with Dirk van Dalen and Walter van Stigt, Heyting described the differences between his and Brouwer’s image of knowledge:
As to your question about Brouwer’s attitude towards formalism, I would like to add that he always maintained that formalizing mathematics is unproductive since mathematics is constructing-in-the-mind, of which language, and therefore also a formal system, can only give inadequate representation. I have become more and more convinced that at least in the communication of mathematics formalization has its great advantages. From recent research into the notion of choice sequences it has become apparent that for any sufficiently clear representation formalization is even necessary. (van Stigt Reference van Stigt1990, 290)
Unlike Brouwer, Heyting viewed the use of formal methods to express intuitionistic ideas as a legitimate technique within the image of mathematical knowledge. As Heyting described in one of his last papers on intuitionism and the nature of mathematics, written in 1974, the formalization of intuitionism had at least two different objectives:
[T]here is a possible application of formal methods to intuitionistic mathematics. It is the best method for investigating the assumptions which are made in a given proof. In recent years it has been successfully applied to the proofs in Brouwer’s theory of choice sequences. The formalization of intuitionistic logic served another purpose, namely to express the logical theorems in a language which is understood by traditional mathematicians. The metamathematical work on the formal system of intuitionistic logic, however interesting in itself, has little to do with intuitionistic mathematics. (Heyting Reference Heyting1974, 89–90)
Heyting viewed the formalization of intuitionism primarily as a tool for mathematical research that could contribute to the development of intuitionistic theories.Footnote 6 His use of axiomatic methods was mostly functional, as a means to an end (the end being the introduction and clarification of Brouwer’s intuitionistic ideas). In his1930 series of papers, Heyting presented his axioms for intuitionistic propositional logic, and in a letter to Oskar Becker, he described how he obtained them:
I sifted the axioms and theorems of Principia Mathematica and, on the basis of those that were found to be admissible, looked for a system of independent axioms. Given the relative completeness of Principia, this to my mind ensures the completeness of my system in the best possible way. Indeed, as a matter of principle, it is impossible to be certain that one has captured all admissible modes of inference in one formal system. (van Atten Reference van Atten and Zalta2017, under “4.4 Heyting 1930”)
Put differently, Heyting developed an intuitionistic system by cutting down a classical axiomatic system to fit the intuitionistic viewpoint. He acknowledged the ability of formal methods to appeal to classical mathematicians and argued that although the use of axiomatic methods is not necessary, it is effective for conveying notions and proofs of intuitionistic mathematics (Heyting Reference Heyting and Heyting1959, 70).
In Heyting’s works, we notice a different kind of change to the body and image of knowledge than that applied in the intuitionistic versions of Brouwer and Weyl. The change Heyting suggested starts from the image of knowledge because he viewed mathematics as a mental activity. However, unlike Brouwer and Weyl, Heyting used the classical body of mathematical knowledge to express his intuitionistic ideas: he presented the philosophical views underlying intuitionistic mathematics through formal axioms. Heyting created a new theory using methods and tools from within the body of knowledge; namely, he used mathematics’ unique ability to absorb a normative view of how mathematics should be properly done into its own body of knowledge.
6. Intuitionism, reflexivity, and body-images
To better understand the differences between the intuitionistic versions of Brouwer, Weyl, and Heyting, let us now return to Corry’s two-tiered approach. As mentioned in section 2, mathematics is endowed with a unique connection between its image and body of knowledge. In mathematics, there is a third, intermediate layer, which involves both the body and image of knowledge, which Corry refers to as reflexive thinking:
Reflexive thinking is clearly a part of the body of mathematical knowledge, because it is produced as any other piece of mathematical knowledge and is justified by proof. On the other hand, it is produced by concentrating on purely second order problems, and hence it is related to the images of knowledge. Mathematical knowledge includes all the layers … [t]hey are in a state of “ongoing dialectical debate” which we must try to understand if we want to understand the historical process of the growth of mathematics. (Corry Reference Corry1989, 425)
Read through Corry’s prism, Heyting’s formalization of intuitionism can be viewed as part of this intermediate layer. Heyting’s use of formal methods to express a philosophical view of mathematical entities as creations of the mind produced a piece of mathematical knowledge that belongs to the body of knowledge but also to the image of knowledge because it concentrates on a normative question of how mathematics should be done.
In clear contrast, Brouwer’s and Weyl’s versions of intuitionism cannot be considered part of this reflexive layer of thought. The changes introduced by both Brouwer and Weyl are changes that concentrate primarily on “second-order problems,” namely, on the layer of the images of knowledge. Unlike Heyting’s intuitionistic mathematics, which affected and involved the body of knowledge as well, the intuitionistic versions suggested by Brouwer and Weyl were confined solely to the normative realm of the images of knowledge.
Neither Brouwer nor Weyl used any methods or theories from the existing body of knowledge to express their intuitionistic ideas. Their point of departure was a normative conception of how mathematics should be properly done, but they did not use formal methods to articulate their intuitionistic approaches. According to Walter van Stigt, even though Brouwer encouraged Heyting to engage with the formalization of intuitionism, Brouwer himself opposed formalization, dismissing it as a “sterile and unproductive mathematical exercise” (van Stigt Reference van Stigt1990, 285).
Heyting’s use of formal methods as tools of communication to convey his intuitionistic ideas serves as a compelling example of the unique connection between mathematics’ body and image of knowledge. Heyting’s intuitionism was rooted in normative considerations, but he also believed that casting them in formal garb rendered some intuitionistic notions clearer and more accessible to the working mathematician. As he wrote:
Intuitionistic mathematics is a mental activity [“Denktätigkeit”], and for it every language, including the formalistic one, is only a tool for communication. It is in principle impossible to set up a system of formulas that would be equivalent to intuitionistic mathematics, for the possibilities of thought cannot be reduced to a finite number of rules set up in advance. Because of this, the attempt to reproduce the most important parts of formal language is justified exclusively by the greater conciseness and determinateness of the latter vis-à-vis ordinary language; and these are properties that facilitate the penetration into the intuitionistic concepts and the use of these concepts in research. (Heyting Reference Heyting and Mancosu1930a, 311)
Heyting’s formalization put intuitionistic logic and classical logic side by side, as two parallel systems, a move that encouraged mathematicians and logicians to develop and analyze the intuitionistic system as well and compare between the two. Indeed, mathematicians were much more inclined to engage with Heyting’s work. Mathematician Alfred Errera and logician Marcel Barzin embarked on a public discussion with Heyting through a series of papers in the L’Enseignement mathematique journal, addressing different aspects of Heyting’s formalization papers (Barzin and Errera Reference Barzin and Errera1931, Reference Barzin and Errera1932a, Reference Barzin and Errera1932b, Reference Barzin and Errera1933). Their correspondence shone a spotlight on Heyting’s work and, in turn, encouraged more mathematicians to interact with it. A quantitative inquiry of the public reactions to intuitionism presented by Dennis Hesseling indicates that in the 1930s, there was a shift in the trajectory and content of the debates; the number of reactions to intuitionism in the 1930s was substantially higher than in the 1920s or earlier. These reactions mainly engaged Heyting’s formalization of logic and not Brouwer’s original intuitionistic program (Hesseling Reference Hesseling2003, 93–99, 363–69).
A substantial amount of the reactions to Heyting’s formalization go beyond the intuitionistic system itself and discuss the differences between classical and intuitionistic mathematics. Mathematician Kurt Gödel and logician and mathematician Gerhard Gentzen each arrived independently at a theorem proving that Peano arithmetic is translatable into Heyting arithmetic (Gödel Reference Gödel, Feferman, Dawson, Kleene, Moore, Solovay and van Heijenoort1933; Gentzen withdrew his paper when he learned of Gödel’s paper). Gödel’s paper concludes: “the system of intuitionistic arithmetic and number theory is only apparently narrower than the classical one, and in truth contains it, albeit with a somewhat deviant interpretation” (Gödel Reference Gödel, Feferman, Dawson, Kleene, Moore, Solovay and van Heijenoort1933, 295). Thus, it seems that Gödel saw the differences between intuitionism and classical mathematics mostly as differences in the image, not the body, of knowledge. Heyting replied to Gödel’s paper, stating that “for the intuitionist, the interpretation is what is essential” (Heyting Reference Heyting1934, 18), and his response made Gödel “supersensitive about differences in meaning” (Kreisel Reference Kreisel, Weingartner and Schmetterer1987, 82; van Atten Reference van Atten and Zalta2017). That is not to imply that Gödel was converted to intuitionism; he certainly was not. But the developments made by Gödel, Gentzen, and Karl Menger (and later by others) to Heyting’s formalized system suggest that Heyting’s formalization of intuitionism allowed for ideas belonging to the intuitionistic image of knowledge to be discussed from within the classical body of knowledge, a discussion that could not have taken place within the contours of Brouwer’s or Weyl’s intuitionistic versions. In order to engage with Brouwer’s intuitionism or Weyl’s intuitionism, mathematicians had to be acquainted, at least to some extent, with their philosophical considerations and understand the implications of such considerations for mathematics. Heyting’s intuitionism offered mathematicians a way to explore intuitionistic ideas without an initial immersion in philosophical commitments they often found foreign and unrelatable.
7. Concluding remarks
This article has proposed viewing the differences between the works of Brouwer, Weyl, and Heyting through the prism of Corry’s dual perspective of a normative and a practical layer of change. Such a perspective concentrates on the normative boundaries of the discipline as each of the three mathematicians conceived it and describes the changes they suggested to the discipline of mathematics in terms of changes to the image and body of knowledge. Brouwer and Weyl suggested a comprehensive change to the image of mathematical knowledge while leaving the classical body of knowledge entirely unaltered. Heyting’s formalization of intuitionism, on the other hand, affected an intermediate layer unique to mathematics through which his image of knowledge was absorbed into the classical body of knowledge.
By applying Corry’s two-tiered model to the works of Brouwer, Weyl, and Heyting, this article polishes the common lens employed by historical and philosophical accounts regarding the differences between the three stories and the reaction of the community to Heyting’s mathematical intuitionism. Philosopher Tomasz Placek argues that Heyting’s nonphilosophical approach renders his intuitionism more approachable and understandable to the practicing mathematician because he is “not distracted by the burden of speculative philosophy” (Placek Reference Placek1999, 106). Mathematician and biographer Walter van Stigt argues that “Heyting’s neo-intuitionism diverges from the Brouwer orthodoxy on three fundamental issues: the philosophical foundation of mathematics, the nature of mathematics as thought-construction, and the role of language and logic in mathematics” (van Stigt Reference van Stigt1990, 275). The current article, however, suggests that there is more to Heyting’s intuitionism than here described. The kind of move Heyting made in formalizing intuitionistic ideas is nonetheless driven by philosophical considerations. Although it is true that Heyting’s philosophical considerations are different from those of Brouwer, the motivation behind Heyting’s formalization is primarily normative, in the sense that his use of formal methods is a means to an end, the end being a representation of how mathematics should be properly done. This objective of his work was marginalized by the formalized system he introduced, as Heyting himself noted in 1978:
They [the 1930s papers] were of little help in the struggle to which I devoted my life, namely a better understanding and appreciation of Brouwer’s ideas. They diverted the attention from the underlying ideas to the formal system itself. (Heyting Reference Heyting1978, 15)
The perspective suggested in this article contributes to existing historical and philosophical accounts by providing an additional aspect to the narrative of the development of intuitionism hitherto left out of the story. It remains true to Heyting’s own intentions in using formal methods to introduce intuitionistic ideas while also providing a possible explanation for mathematicians’ inclination to engage with, develop, and respond to Heyting’s version of intuitionism.
Brouwer, Weyl, and Heyting each held a different view regarding the proper way of doing mathematics, and those differences translated into three different versions of intuitionism. Unlike Brouwer’s intuitionism and Weyl’s intuitionism, Heyting’s mathematical intuitionism affected the classical body of knowledge by absorbing into it an intuitionistic image of knowledge, thereby creating a mathematical theory that is part of both layers. Among the three, Heyting was the only one who used formal methods from the classical body of knowledge to express his intuitionistic mathematics, thereby creating a way for classical mathematicians to discuss intuitionistic ideas. This perspective, therefore, enriches current historical and philosophical accounts, and when all are considered together, they combine to offer a more comprehensive account of the intuitionistic story and its reception than any can offer alone.
