The Development of Intuitionistic Logic

First published Thu Jul 10, 2008; substantive revision Wed Nov 8, 2017
“Intuitionistic logic” is a term that unfortunately gains ever greater currency; it conveys a wholly false view on intuitionistic mathematics. —Freudenthal 1937

Intuitionistic logic is an offshoot of L.E.J. Brouwer’s intuitionistic mathematics. A widespread misconception has it that intuitionistic logic is the logic underlying Brouwer’s intuitionism; instead, the intuitionism underlies the logic, which is construed as an application of intuitionistic mathematics to language. Intuitionistic mathematics consists in the act of effecting mental constructions of a certain kind. These are themselves not linguistic in nature, but when acts of construction and their results are described in a language, the descriptions may come to exhibit linguistic patterns. Intuitionistic logic is the mathematical study of these patterns, and in particular of those that characterize valid inferences. An inference rule is valid if, whenever the statements in the premises describe truths of intuitionistic mathematics, a construction can be found that makes true the statement that is obtained by applying the rule. What the principles of logic need to preserve is therefore not, as in classical logic, mind-independent truth, but mental constructibility. Various principles of classical logic, most notably the Principle of the Excluded Middle, then become insufficiently grounded, and certain classical theorems even contradictory. The theorems in intuitionistic logic that formally contradict classical theorems depend on elements of intuitionistic mathematics that are incompatible with classical mathematics; this illustrates how in intuitionism logic is based on mathematics and not the other way around.

The systematic explanation and formalization of intuitionistic logic was begun by Brouwer’s student Arend Heyting in 1928. An “explanation” here is an account of what one knows when one understands and correctly uses the logical connectives. Since the 1970s Heyting’s explanation and its variants are known as “the Proof Interpretation”, as the role played by mind-independent truth in explanations of classical logic is here played by proof. For Heyting, a proof was primarily a mathematical construction in Brouwer’s sense, and, secondarily, a linguistic description of it. But it turned out that a Proof Interpretation can also be based on other notions of proof. The Proof Interpretation understood in a more general sense has found many applications outside its historical origin, notably in other constructive but non-intuitionistic forms of mathematics, philosophy, computer science, and linguistics. This widening of the range of application was possible because the original Proof Interpretation depends mostly on the fact that the intuitionistic notion of mathematical truth is of a verificationist nature, so that broadly verificationist theories in other domains allow for an analogous explanation of their logic.

In this article, the principal concern is with the development of the Proof Interpretation within its original context of intuitionistic mathematics. Section 1 comments on terminology. Section 2 examines the basis of Brouwer’s conception of logic in his early writings. Section 3 presents his later refinements and also his views on Hilbert’s Program, Gödel’s incompleteness theorems, and the debate in the foundations of mathematics in the 1920s. Section 4 discusses formalizations of intuitionistic logic, which had begun even before the Proof Interpretation had been made explicit, and briefly looks at mathematical interpretations of the formalisms obtained. The explanation of the Proof Interpretation in Heyting’s writings from 1930 to 1956 is treated in section 5. The sensitivity of intuitionistic logic to the exact conception of mathematical construction was at the root of strong objections to parts of the Proof Interpretation that arose from within intuitionism. These are discussed in section 6. At the end, a short list is given of topics that will be added in future updates.

1. Introduction

1.1 The Proof Interpretation

The standard explanation of intuitionistic logic today is the BHK-Interpretation (for “Brouwer, Heyting, Kolmogorov”) or Proof Interpretation as given by Troelstra and van Dalen in Constructivism in Mathematics (Troelstra & van Dalen 1988: 9):

  • (H1)A proof of \(A \wedge B\) is given by presenting a proof of \(A\) and a proof of \(B\).
  • (H2)A proof of \(A \vee B\) is given by presenting either a proof of \(A\) or a proof of \(B\) (plus the stipulation that we want to regard the proof presented as evidence for \(A \vee B\)).
  • (H3)A proof of \(A \rightarrow B\) is a construction which permits us to transform any proof of \(A\) into a proof of \(B\).
  • (H4)Absurdity \(\bot\) (contradiction) has no proof; a proof of \(\neg A\) is a construction which transforms any hypothetical proof of \(A\) into a proof of a contradiction.
  • (H5)A proof of \(\forall xA(x)\) is a construction which transforms a proof of \(d \in D\) (\(D\) the intended range of the variable \(x)\) into a proof of \(A(d)\).
  • (H6)A proof of \(\exists xA(x)\) is given by providing \(d \in D\), and a proof of \(A(d)\).

Notions such as “construction”, “presenting” and “transformation” can be understood in different ways, and indeed they have been. Similarly, there have been different ideas as to how one may justify that concrete instances of clauses H3 and H4 indeed work for any (possibly hypothetical) proof of the antecedent. Logical principles that are valid on one understanding of these notions may not be valid on another. As Troelstra and van Dalen indicate, it is even possible to understand these clauses in such a way that they validate the principles of classical logic (Troelstra & van Dalen 1988: 9, 32–33; see also Sundholm 2004 and Sato 1997). In the context of the foundational programs of intuitionism and constructivism, all notions are of course understood to be effective; but even then there is room for differences of understanding. Such differences can have mathematical consequences. On some understandings, intuitionistic logic turns out formally to be a subsystem of classical logic (namely, classical logic without the Principle of the Excluded Middle). But that is not the understanding of intuitionistic mathematicians, who, in analysis, have constructed intuitionistically valid instances of the schema \(\neg \forall x(Px \vee \neg Px)\), while classically there can be none (see the section on Strong counterexamples and the Creating Subject (3.3), below).

Troelstra and van Dalen specify that the clauses H1–H6 go back to Heyting’s explanation from 1934 (hence “H”). Heyting’s aim had been to clarify the conception of logic in Brouwer’s foundational program in mathematics, which would motivate adding the following clause:

  • (H0) A proof of an atomic proposition \(A\) is given by presenting a mathematical construction in Brouwer’s sense that makes \(A\) true.

Indeed, as we will see, a version of the Proof Interpretation is implicit already in Brouwer’s early writings from 1907 and 1908, and was notably used by him in his proofs of the bar theorem from 1924 and 1927, which predate Heyting’s papers on logic. We will therefore begin our account of the historical development of intuitionistic logic with Brouwer’s ideas, and then show how, via Heyting and others, the modern Proof Interpretation was arrived at.

1.2 Interpretation, Explanation, and Names

As Sundholm (1983: 159) points out, in the terms “BHK-Interpretation” and “Proof Interpretation” it would be appropriate to replace “Interpretation” by “Explanation”. For in a logical-mathematical context, “interpretation” has come to refer to the interpretation of one formal theory in another.[1] An interpretation of a formal system \(U\) in a formal system \(V\) is given by a translation \('\) of formulas of \(U\) to formulas of \(V\) that preserves provability:[2]

\[ \textrm{If } U \vdash A \textrm{ then } V \vdash A' \]

For the moment, we note that the BHK-Interpretation or Proof Interpretation is not an interpretation in this mathematical sense, but is rather a meaning explanation; we will come back to such interpretations and their difference from explanations in section 4.5.2 below.

While accepting Sundholm’s point, we keep the terms themselves, considering that they have perhaps become too common to change. Section 5.3 below is the appropriate place to explain our preference for “Proof Interpretation” over “BHK-Interpretation”.

The name “Proof Interpretation” for the explanation that Heyting published in the 1930s and later seems to have made its first appearance in print only in 1973, in papers by van Dalen and Kleene, presented at the same conference (van Dalen 1973a; Kleene 1973). Heyting himself spoke simply of the “interpretation” (1958A: 107; 1974: 87) or “the intuitionistic interpretation” (1958A: 110) of logic.

The name “BHK-Interpretation” was coined by Troelstra (1977: 977), where “K” initially stood for “Kreisel” (because of Kreisel 1962), later for “Kolmogorov”, e.g., in Troelstra 1990: 6; this replacement is, in keeping with Sundholm’s point, a correction.

2. Brouwer’s Views on Logic in 1907 and 1908

2.1 Mathematics, Language, and Logic

In his dissertation (1907), Brouwer presents his conception of the relations between mathematics, language, and logic. Both the intuitionistic view of logic as essentially sterile, and the existence of results in intuitionistic logic that are incompatible with classical logic, depend essentially on that conception.

For Brouwer, pure mathematics consists primarily in the act of making certain mental constructions (Brouwer 1907: 99n.1 [1975: 61n.1).[3] The point of departure for these constructions is the intuition of the flow of time.[4] This intuition, when divested from all sensuous content, allows us to perceive the form “one thing and again a thing, and a continuum in between”. Brouwer calls this form, which unites the discrete and the continuous, “the empty two-ity”. It is the basic intuition of mathematics; the discrete cannot be reduced to the continuous, nor the continuous to the discrete (Brouwer 1907: 8 [1975: 17]).

As time flows on, an empty two-ity can be taken as one part of a new two-ity, and so on. The development of intuitionistic mathematics consists in the exploration which specific constructions the empty two-ity and its self-unfolding or iteration allows and which not:

The only possible foundation of mathematics must be sought in this construction under the obligation carefully to watch which constructions intuition allows and which not. (Brouwer 1907: 77 [1975: 52])

or, in Heyting’s words,

[Brouwer’s] construction of intuitionist mathematics is nothing more nor less than an investigation of the utmost limits which the intellect can attain in its self-unfolding. (Heyting 1968A: 314)

Brouwer and other intuitionists have shown how on this basis arithmetic, real analysis, and topology can be constructed. Moreover, Brouwer considers any exact thought that is not itself mathematics an application of mathematics. For whenever we consciously think of two things together while keeping them separate, we do so, according to Brouwer, by projecting the empty two-ity on them (Brouwer 1907: 179n.1 [1975: 97n.1]).

Brouwer takes the intuition of time to belong to pre-linguistic consciousness. Mathematics, therefore, is essentially languageless. It is the activity of effecting non-linguistic constructions out of something that is not of a linguistic nature. Using language we can describe our mathematical activities, but these activities themselves do not depend on linguistic elements, and nothing that is true about mathematical constructional activities owes its truth to some linguistic fact. Linguistic objects such as axioms may serve to describe a mental construction, but they cannot bring it into being. For this reason, certain axioms from classical mathematics are rejected by intuitionists, such as the completeness axiom for real numbers, which says that if a non-empty set of real numbers has an upper bound, then it has a least upper bound: we know of no general method that would allow us to construct mentally the least upper bound whose existence the axiom claims.

As Brouwer later put it, “Formal language accompanies mathematics as a score accompanies a symphony by Bach or an oratorio by Handel”. (Brouwer et al. 1937: 262; translation mine)[5] Correspondingly, establishing properties of formal systems may have many uses, but ultimately has no foundational significance for mathematics. In a lecture from 1923, Brouwer expresses optimism about Hilbert’s proof theory, but denies that it would have significance for mathematics:

We need by no means despair of reaching this goal [of a consistency proof for formalized mathematics], but nothing of mathematical value will thus be gained: an incorrect theory, even if it cannot be inhibited by any contradiction that would refute it, is none the less incorrect, just as a criminal policy is none the less criminal even if it cannot be inhibited by any court that would curb it. (Brouwer 1924N: 3 [van Heijenoort 1967: 336])

At the same time, Brouwer was well aware of the practical need for language, both in order to communicate mathematical results to others and to help ourselves in remembering and reconstructing our previous results (Brouwer 1907: 169 [1975: 92]). Only an ideal mathematician with perfect and unlimited memory would be able to practice pure mathematics without recourse to language (Brouwer 1933A2: 58 [van Stigt 1990: 427]). Clearly, given these two practical functions of language, the more precise the language is, the better.

Logic, in this framework, seeks and systematizes certain patterns in the linguistic recordings of our activities of mathematical construction. It is an application of mathematics to the language of mathematics. Specifically, logic studies the patterns that characterize valid inference. The aim is to establish general rules operating on statements about mathematical constructions such that, if the original statements (the premises) convey a mathematical truth, so will the statement obtained by applying the rule (the conclusion; Brouwer 1949C: 1243). What is preserved in an inference from given premises to a conclusion is therefore not, as in classical logic, a kind of possibly evidence-transcendent truth, but constructibility. This view is quite explicit already in Brouwer’s dissertation (Brouwer 1907: 125–132, 159–160 [1975: 72–75, 88]), but a more memorable passage is in the paper from 1908:

Can one, in the case of purely mathematical constructions and transformations, temporarily neglect the presentation of the mathematical system that has been erected, and move in the accompanying linguistic building, guided by the principles of the syllogism, of contradiction, and of tertium exclusum, always confident that, by momentary evocation of the presentation of the mathematical constructions suggested by this reasoning, each part of the discourse could be justified? (Brouwer 1908C: 4 [van Atten & Sundholm 2017: 40])

(He then goes on to argue that the answer is “yes” for the principles of the syllogism and of contradiction, but, in general, “no” for the Principle of the Excluded Middle (PEM); more on this below, section 2.4.)

But if a certain mathematical construction can be constructed out of another one, this is a purely mathematical fact, and as such independent of logic. Logic therefore is descriptive but not creative: by the use of logic, one will never obtain mathematical truths that are not obtainable by a direct mathematical construction (Brouwer 1949C: 1243). Hence, in the development of intuitionistic mathematics, logic can never play an essential role. It follows from Brouwer’s view that logic is subordinate to mathematics. The classical view that mathematics is subordinate to logic is closely related to the view that pure logic has no particular subject matter or domain, and is prior to all. From that perspective, Brouwer’s conception of logic as dependent on mathematics will seem too restrictive. But for Brouwer logic always presupposes mathematics, because in his view it is, like any exact thought, an application of mathematics.

The resulting linguistic system of logic may in turn be studied mathematically, even independently of the mathematical activities and their recordings that it was originally abstracted from. Iterating the process, an infinite hierarchy arises of mathematical activities, their linguistic recordings, and the mathematical study of these recordings as linguistic objects independently of their original meaning. Brouwer describes this hierarchy (in more detail than we have done here) at the end of his dissertation (Brouwer 1907: 173ff), and criticizes Hilbert for not respecting it. Of particular interest is the distinction Brouwer makes between mathematics and “mathematics of the second order” (Brouwer 1907: 99n.1, 173 [1975: 61n.1, 94]), where the latter is the mathematical study of the language of the former in abstraction from its original meaning; this way, Brouwer made fully explicit the distinction between mathematics and (what became known as) metamathematics (e.g., Hilbert 1923: 153). Later, Brouwer claimed priority for this distinction, adding in a footnote that he had explained it to Hilbert in a series of conversations in 1909 (Brouwer 1928A2: 375 [Mancosu 1998: 44n.1]).

2.2 The Hypothetical Judgement

Brouwer realized (1907: 125–128 [1975: 72–73]) that the hypothetical judgement seems to pose a problem for his view on logic as described above. For what is peculiar to the hypothetical judgement, Brouwer says, is that there the priority of mathematics over logic seems to be reversed. Among the examples he refers to are the proofs found in elementary geometry of the problems of Apollonius. Here is one of them: Given three circles, defined by their centers and their radii, construct a fourth circle that is tangent to each of the given three. The way this is usually solved is first to assume that such a fourth circle exists, then to set up equations that express how it is related to the three given circles, and then, via algebraic manipulations and logic, arrive at explicit definitions of the center and radius of the required circle, and, from there, at corresponding mathematical constructions. So it seems that here one first has to assume the existence of the required circle, then use logic to make various judgements about it, and only thereby arrives at a mathematical construction for it.

However, Brouwer argues, this is not what really happens. His general interpretation of such cases is as follows. Having first remarked that logical reasoning accompanies or mirrors mathematical activity which is at least conceptually prior to that reasoning, Brouwer then says:

There is a special case […] which really seems to presuppose the hypothetical judgment from logic. This occurs where a structure in a structure is defined by some relation, without it being immediately clear how to effect its construction. Here one seems to assume to have effected the required construction, and to deduce from this hypothesis a chain of hypothetical judgments. But this is no more than apparent; what one is really doing in this case is the following: one starts by constructing a system that fulfills part of the required relations, and tries to deduce from these relations, by means of tautologies, other relations, in such a way that in the end the deduced relations, combined with those that have not yet been used, yield a system of conditions, suitable as a starting-point for the construction of the required system. Only by this construction will it then have been proved that the original conditions can indeed be satisfied. (Brouwer 1907: 126–127 [1975: 72; translation modified])

Different readings of this concise passage have been proposed. According to one, Brouwer’s passage bears on \(A \rightarrow B\) in the following way:

  • \((\alpha)\) Brouwer points out in the above lines that if the conditions and specifications for \(A\) are given, then we try to add more information in such a way that, after a certain amount of constructional activity, we can really carry out a construction of \(A\) which respects the specifications. Once this is accomplished, we can turn to the “implication” construction for \(B\), which yields the construction for \(B\) and to the required embedding of the structure for \(A\) into the structure for \(B\). (van Dalen 2004: 250–251)

According to interpretation \(\alpha\), \(A \rightarrow B\) just means \(A \wedge B\) with the extra information that the construction for \(B\) was obtained from that for \(A\). On this reading \(A \rightarrow B\) can be asserted only after a construction for \(A\) has been found. The idea is clear: namely, to avoid hypothetical constructions, and the use of logic they require, by insisting that a construction be supplied that proves the antecedent. (As will be explained in section 6.2.1 below, Freudenthal (1937b) too has suggested this strategy, albeit with a different motivation than this passage in Brouwer’s dissertation.) But, as van Dalen also notices, it is also in effect a rejection of the hypothetical judgement in the general case where one does not know whether there is a construction for \(A\).

An alternative reading is \(\beta\):

  • \((\beta)\) In order to establish \(A \rightarrow B\), one has to conceive of \(A\) and \(B\) as conditions on constructions, and to show that from the conditions specified by \(A\) one obtains the conditions specified by \(B\), according to transformations whose composition preserves mathematical constructibility. (van Atten 2009: 128)

On this reading, Brouwer’s explanation of the hypothetical judgement avoids hypothetical constructions and the concomitant use of logic by considering conditions on constructions instead of constructions themselves. Instead of a “chain of hypothetical judgements” that one seems to make, one is really making a chain of transformations in which from required relations (i.e., given conditions) further relations are derived. It is, of course, a requirement that these transformations preserve mathematical constructibility, and that this preservation is itself intuitively known. The role of conditions is explicit in a statement Brouwer made at the other end of his publishing career:

[T]he wording of a mathematical theorem has no sense unless it indicates the construction either of an actual mathematical entity or of an incompatibility (e.g., the identity of the empty two-ity with an empty unity) out of some constructional condition imposed on a hypothetical mathematical system. (Brouwer 1954A: 3)

Brouwer speaks not of an incompatibility constructed out of a hypothetical mathematical system, but out of some condition on its construction.

Be that as it may, the preservation of constructibility from \(A\) to \(B\) is essential to both reading \(\alpha\) and reading \(\beta\), so on either it is clear that Brouwer had the Proof Interpretation of the implication in mind already in 1907. For further discussion of Brouwer’s passage on the hypothetical judgement and the two readings of it mentioned here, see Kuiper 2004, van Dalen 2004, van Atten 2009, and van Dalen 2008.

2.3 Negation

Intuitionistically, to say that a proposition \(A\) is true is primarily to say that we have effected a construction that is correctly described by \(A\); the proposition \(A\) is made true by the construction. Idealizing to a certain extent, we say that \(A\) is true if we possess a construction method that, when effected, will yield a construction that is correctly described by \(A\). According to Brouwer, to say that a proposition \(A\) is false then must mean that it is impossible to effect an appropriate construction; notation \(\neg A\). Such an impossibility is recognized either immediately (e.g., the impossibility to identify 1 unit and 2 units) or mediately. In the former case, one observes directly that an intended construction is blocked; it “does not go through” (Brouwer 1907: 127 [1975: 73]). In the latter case, one shows that a proposition \(A\) is contradictory by reducing \(A\) to a known falsehood, e.g., one shows that \(A \rightarrow 1=2\) (Brouwer 1954A: 3). In practice, one defines \(\neg A := A \rightarrow 1=2\) (and hence \(\neg 1=2\) is seen as a particular case of \(A \rightarrow A)\).

The notion of “negation as impossibility” is known as “strong negation”. One speaks of the “weak negation” of \(A\) to express that so far no proof of \(A\) has been found. This excludes neither finding a proof of \(A\) nor finding a proof of \(\neg A\) later. Clearly, then, to assert the weak negation of \(A\) is not to assign a truth value besides true and false to it; Barzin and Errera’s claim (see section 4.3 below) that its treatment of negation turns Brouwer’s logic into a three-valued one is groundless. The distinction between weak and strong negation is important for the so-called “weak counterexamples”.

2.4 Weak Counterexamples (“unreliability”) and Excluded Middle

As the rules of logic operate on linguistic objects, and these linguistic objects may be considered separately from the precise mathematical context in which they described a truth, it is possible to apply the rules of logic and obtain new linguistic objects without providing a precise mathematical context for the latter. In other words, the logical principles, which can be stated without specifying the context in which they are applied, and thereby suggest context-independence, are for their correctness sensitive to the context. There is no general guarantee that logical principles which are valid in one context, will be equally valid in a different one. This is what Brouwer means when he speaks of “the unreliability of the logical principles”, the title and theme of his seminal paper Brouwer 1908C; see also Brouwer 1949A: 1243.

In that paper, Brouwer draws a consequence of his general view on logic that he had overlooked in his dissertation: PEM, \(A \vee \neg A\), is not valid. Its constructive validity would mean that we have a method that, for any \(A\), either gives us a construction for \(A\), or shows that such a construction is impossible. But we do not have such a general decision method, and there are many open problems in mathematics. Brouwer states “Every number is finite or infinite” as an example of a general proposition for which so far no constructive proof has been found. As a consequence, he says, it is at present uncertain whether problems such as the following are solvable:

Is there in the decimal expansion of \(\pi\) a digit which occurs more often than any other one?

Do there occur in the decimal expansion of \(\pi\) infinitely many pairs of equal consecutive digits? (Brouwer 1908C: 7 [van Atten & Sundholm 2017: 44])

In effect, Brouwer is saying that we can assert the weak negations of the propositions expressed in these questions; hence, these propositions are so-called “Brouwerian counterexamples” or “weak counterexamples” to PEM. On the constructive reading of PEM, of course any as yet unsolved problem is a weak counterexample to PEM. Brouwer began to publish weak counterexamples to PEM in international journals only much later (1921A, 1924N, 1925E).

Brouwer remarks in the 1908 paper that the fact that PEM is not valid does not mean that it is false: \(\neg(A \vee \neg A)\) implies \(\neg A \wedge \neg \neg A\), a contradiction. In other words, \(\neg \neg(A \vee \neg A)\) is correct. Brouwer concludes that it is always consistent to use PEM but that it does not always lead to truths. In the latter case, the argument that appeals to PEM establishes not the truth, but the consistency of its conclusion. Brouwer proposes to divide the theorems that are usually considered as proved into the true and the non-contradictory ones (Brouwer 1908C: 7n.2 [van Atten & Sundholm 2017: 44n.14]). That is not a suggestion that there are three truth values, true, non-contradictory, false; for a non-contradictory proposition might be proved one day and thereby become true.

A mathematical context in which PEM is valid, Brouwer points out, is that of the question whether a given construction of finite character is possible in a given finite domain. In such a context there are only finitely many possible attempts at that construction, and each will succeed or fail in finitely many steps (for clarity, the phrasing here is not that of Brouwer 1908C but that of Brouwer 1955). So on these grounds \(A \vee \neg A\) holds, where \(A\) is the proposition stating that the construction exists.

Brouwer ascribed the belief in the general validity of PEM to an unwarranted projection from such finite cases (in particular, those arising from the application of finite mathematics to everyday phenomena) to the infinite.[6]

In his dissertation of 1907, Brouwer still accepted PEM as a tautology, understanding \(A \vee \neg A\) as \(\neg A \rightarrow \neg A\) (Brouwer 1907: 131, 160 [1975: 75, 88]).[7] Curiously, he did realize at the same time that there is no evidence for the principle that every mathematical proposition is either provable or refutable (Brouwer 1907: 142n.3 [1975: 101]); this principle is the constructively correct reading of PEM. In the paper from 1908, he corrected his earlier understanding of PEM:

Now the principium tertii exclusi: this demands that every supposition is either correct or incorrect, mathematically: that of every supposed fitting in a certain way of systems in one another, either the termination or the blockage by impossibility, can be constructed. (Brouwer 1908C: 5 [van Atten & Sundholm 2017: 42])

2.5 There Are No Absolutely Undecidable Propositions

Brouwer continues this last quotation as follows:

It follows that the question of the validity of the principium tertii exclusi is equivalent to the question whether unsolvable mathematical problems can exist. There is not a shred of proof for the conviction, which has sometimes been put forward [here Brouwer refers in a footnote to Hilbert 1900] that there exist no unsolvable mathematical problems.

Here he seems to overlook that, constructively, there is a difference between the claim that every mathematical problem is solvable and the weaker claim that there are no absolutely unsolvable problems. The former is equivalent to \(A \vee \neg A\), the latter to \(\neg \neg(A \vee \neg A)\); and Brouwer had demonstrated the intuitionistic validity of the latter in the same paper. Indeed, in the Brouwer archive there is a note from about the same period 1907–1908 in which the point is made explicitly:

Can one ever demonstrate of a proposition, that it can never be decided? No, because one would have to so by reductio ad absurdum. So one would have to say: assume that the proposition has been decided in sense \(a\), and from that deduce a contradiction. But then it would have been proved that not-\(a\) is true, and the proposition is decided after all. (van Dalen 2001b: 174n.a; translation mine)

Brouwer never published this note. Wavre in 1926 gave the argument for a particular case, clearly seeing the general point:

It suffices to give an example of a number of which one does not know whether it is algebraic or transcendent in order to give at the same time an example of a number that, until further information comes in, could be neither the one nor the other. But, on the other hand, it would be in vain, it seems to me, to want to define a number that indeed is neither algebraic nor transcendent, as the only way to show that it is not algebraic consists in showing that it is absurd that it would be, and then the number would be transcendent. (Wavre 1926: 66; translation mine)

The explicit observation that \(\neg \neg(A \vee \neg A)\) means that no absolutely unsolvable problem can be indicated was made in Heyting 1934: 16.

3. Brouwer’s Later Refinements and Applications, 1921–1955

3.1 The Implicit Proof Interpretation

Three examples can be given that show that by the mid-1920s, Brouwer in practice worked with the hypothetical judgement and with the clause for implication in the Proof Interpretation (which was published later): an equivalence in propositional logic, the proof of the bar theorem, and his reading of ordering axioms.

3.1.1 An equivalence in propositional logic

In a lecture in 1923, Brouwer presented a proof of \(\neg \neg \neg A \leftrightarrow \neg A\) (Brouwer 1925E: 253 [Mancosu 1998: 291]).[8] This equivalence is the one theorem in propositional logic that Brouwer ever published. The argument begins by pointing out that \(A \rightarrow B\) implies that \(\neg B \rightarrow \neg A\) (because \(\neg B\) is \(B \rightarrow \bot\) and the two implications can be composed because the consequent of the one is the antecedent of the other). It would not have been possible for Brouwer to make this inference if at the time it would have been among his proof conditions of an implication to have a proof of the antecedent, as then a proof of \(A \rightarrow B\) would lead to a proof of \(B\) and thereby make it impossible to begin establishing the second implication by proving its antecedent \(\neg B\).

Later, Brouwer pointed out the following consequence of the validity of \(\neg \neg \neg A \leftrightarrow \neg A\): the proof method of reductio ad absurdum can be used to establish negative propositions \(\neg A\) (Brouwer 1929A: 163 [Mancosu 1998: 52]). For if the assumption of \(\neg \neg A\) leads to a contradiction, that is, to \(\neg \neg \neg A\), the equivalence allows one to simplify that to \(\neg A\). On the other hand, reductio ad absurdum in general cannot be used to establish positive propositions \(A\); the derivation of a contradiction from the assumption \(\neg A\) only leads to \(\neg \neg A\), which intuitionistically is weaker than \(A.\)

3.1.2 The proof of the bar theorem

Brouwer’s bar theorem is crucial to intuitionistic analysis; for a detailed explanation of the notions involved and of Brouwer’s proof, see Heyting 1956 (Ch. 3), Parsons 1967, and van Atten 2004b (Ch. 4). Here we will rather be concerned with the logical aspects.

Brouwer’s proof of the bar theorem from 1924 (later versions of the proof appeared in 1927 and in 1954) proves a statement of the form “If \(A\) has been demonstrated, then \(B\) is demonstrable” (Brouwer 1924D1, 1927B, 1954A). This is evidently not the same as an implication \(A \rightarrow B\) understood as a transformation of the proof conditions of \(A\) into those of \(B\), because in the former case there is the additional information that, by hypothesis, \(A\) has been demonstrated. In other words, we have, by hypothesis, a concrete proof of \(A\) at hand. (However, both are hypothetical judgements in the sense that neither requires that we actually have demonstrated \(A\).) It may be possible to exploit this extra information, and below it will be indicated how Brouwer did this. (Heyting in 1956 chose to define implication in this stronger sense; see section 5.4 below.)

The statement in question can be rendered more specifically as

If it has been demonstrated that tree \(T\) contains a set of nodes forming a bar, then it can be demonstrated that \(T\) contains a bar that is well-ordered.[9]

Brouwer first formulates a condition for any demonstration that may be found of the proposition “Tree \(T\) contains a bar”. This condition is that any demonstration of that proposition must be analyzable into a certain canonical form. Brouwer then gives a method to transform any such demonstration, when analyzed into that canonical form, into a mathematical construction that makes the proposition “\(T\) contains a well-ordered bar”, true, thereby establishing the consequent. This strategy clearly shows that Brouwer’s operative explanation of the meaning of \(A \rightarrow B\) was a version of clause (H3) of the Proof Interpretation as formulated in the Introduction, if we understand “proof” in that clause as “demonstration”.

A demonstration or concrete proof of the antecedent, be it an actual or a hypothetical one, is required to obtain a canonical form. The reason is that the existence of a canonical proof of a proposition \(A\) cannot be logically derived from the mere proof conditions of \(A\), as the form such a canonical proof takes may well depend on specific non-logical details of mathematical constructions for \(A\).

In Brouwer’s proof of the bar theorem, the applicability of the transformation method to any demonstration of the antecedent is guaranteed by the fact that the condition on such demonstrations that he formulates is a necessary condition. Brouwer obtained this necessary condition by exploiting the fact that on his conception, mathematical objects, so in particular trees and bars, are mental objects; this opens the possibility that reflection on the way these objects and their properties are constructed in mental acts provides information on them that can be put to mathematical use, in particular if this information consists in constraints on these acts of construction. This is how Brouwer arrived at his canonical form. In effect, Brouwer’s argument for the bar theorem is a transcendental argument. On other conceptions of mathematics such considerations need not be acceptable, and indeed no proofs of the (classically valid) bar theorem are known in other varieties of constructive mathematics (where bar induction is either accepted as an axiom, a possibility that Brouwer had also suggested (Brouwer 1927B: 63n.7 [van Heijenoort 1967: 460n.7]), or not accepted, as in the Markov School).

For a more detailed discussion of this matter, see Sundholm and van Atten 2008.

3.1.3 Ordering axioms

Around 1925, Brouwer introduced the notion of “virtual ordering”. A (partial) ordering \(\lt\) is virtual if it satisfies the following axioms (Brouwer 1926A: 453):

  1. The relations \(r = s, r \lt s\) and \(r \gt s\) are mutually exclusive.
  2. From \(r = u, s = v\) and \(r \lt s\) follows \(u \lt v\).
  3. From the simultaneous failure of the relations \(r \gt s\) and \(r = s\) follows \(r \lt s\).
  4. From the simultaneous failure of the relations \(r \gt s\) and \(r \lt s\) follows \(r = s\).
  5. From \(r \lt s\) and \(s \lt t\) follows \(r \lt t\).

In a lecture course on Order Types in 1925, of which David van Dantzig’s notes are preserved in the Brouwer Archive, Brouwer commented:

The axioms II through V are to be understood in the constructive sense: if the premisses of the axiom are satisfied, the virtually ordered set should provide a construction for the order condition in the conclusion. (van Dalen 2008: 19)

This is a clear instance of the clause for implication in the Proof Interpretation. Note that Brouwer did not include this elucidation in the published paper (1926A), nor in later presentations.

3.2 Widening the Scope of the Weak Counterexamples

As we saw above, in the paper from 1908 Brouwer had given weak counterexamples to PEM. In the 1920s Brouwer developed a general technique for constructing weak counterexamples which also made it possible to widen their scope and include principles of analysis. The development began in 1921, when Brouwer gave a weak counterexample to the proposition that every real number has a decimal expansion (Brouwer 1921A). The argument proceeded by defining real numbers whose decimal developments are dependent on specific open problems concerning the decimal development of \(\pi\). Brouwer closed by observing that, should these open problems be solved, then other real numbers without decimal expansion can be defined (Brouwer 1921A: 210 [Mancosu 1998: 34]). The general technique was made explicit in a lecture from 1923 (Brouwer 1924N: 3 and footnote 4 [van Heijenoort 1967: 337 and footnote 5]) and reached its perfection with the “oscillatory number” method in the first Vienna lecture in 1928 (Brouwer 1929A: 161 [Mancosu 1998: 51]). The method involves the reduction of the validity of a mathematical principle to the solvability of an open problem of the following type: we have a decidable property \(P\) (defined on the natural numbers) for which we have as yet shown neither \(\exists xP(x)\) nor \(\forall x\neg P(x)\). This reduction is carried out in such a way that it only uses the fact that \(P\) induces an open problem of this type, and does not depend on the exact definition of \(P\); that is, if the open problem is solved, one can simply replace it by another one (of the same type), and exactly the same reduction still works. This uniformity means that, as long as there are open problems of this type at all (and this is practically certain at any time), there is no intuitionistic proof of the general mathematical principle in question. In the 1920s, Brouwer constructed weak counterexamples to the following general mathematical propositions, among others (where \(\mathbf{R}\) stands for the set of intuitionistic real numbers, and \(\mathbf{Q}\) for the set of rationals):

  1. The continuum is totally ordered (Brouwer 1924N)
  2. Every set is either finite or infinite (Brouwer 1924N)
  3. The Heine-Borel theorem (Brouwer 1924N)
  4. \(\forall x \in \mathbf{R}(x \in \mathbf{Q} \vee x \not\in \mathbf{Q})\) (Brouwer 1925E)
  5. Any two straight lines in the Euclidean plane are either parallel, or coincide, or intersect (Brouwer 1929A)
  6. Every infinite sequence of positive numbers either converges or diverges (Brouwer 1929A)

3.3 Strong Counterexamples and the Creating Subject

A weak counterexample shows that we cannot at present prove some proposition, but it does not actually refute it; in that sense, it is not a counterexample proper. From 1928 on, Brouwer devised a number of strong counterexamples to classically valid propositions, that is, he showed that these propositions were contradictory. This should be understood as follows: if one keeps to the letter of the classical principle but in its interpretation substitutes intuitionistic notions for their classical counterparts, one arrives at a contradiction. So Brouwer’s strong counterexamples are no more counterexamples in the strict sense of the word than his weak counterexamples are (but for a different reason). One way of looking at strong counterexamples is that they are non-interpretability results.

That strong counterexamples to classical principles are possible at all is explained as follows. As mentioned, on the intuitionistic understanding, logic is subordinate to mathematics, whereas classically it is the other way around. Hence, if intuitionistic mathematics contains objects and principles that do not figure in classical mathematics, it may come about that intuitionistic logic, which then depends also on these non-classical elements, is no proper part of classical logic.

Brouwer’s first strong counterexample was published in Brouwer 1928A2, where he showed:

\[ \neg \forall x\in \mathbf{R}(x \in \mathbf{Q} \vee x \not\in \mathbf{Q}) \]

This is a strengthening of the corresponding weak counterexample from 1923, but the argument is entirely different. The strong counterexample depends on the theorem in intuitionistic analysis, obtained in 1924 and improved in 1927, that all total functions \([0,1] \rightarrow \mathbf{R}\) are uniformly continuous. The non-classical elements in that theorem are the conception of the continuum as a spread of choice sequences, and the Bar Theorem based on it (for further explanations of this conception, see Heyting 1956 (Ch.3) and van Atten 2004b (Chs.3 and 4)).[10]

From 1948 on, Brouwer also published counterexamples that are based on so-called “creating subject methods”. (He mentions in Brouwer 1948A that he has been using this method in lectures since 1927.) Their characteristic property is that they make explicit reference to the subject who carries out the mathematical constructions, to the temporal structure of its activities, and the relation of this structure to the intuitionistic notion of truth. These methods can be used to generate weak as well as strong counterexamples. (In the earlier “oscillatory number” method for generating weak counterexamples, the creating subject is not explicitly referred to.)

Using creating subject methods, Brouwer showed, for instance,

\[ \begin{align*} \neg \forall x & \in \mathbf{R}(\neg \neg x \gt 0 \rightarrow x \gt 0) & \textrm{(Brouwer 1949A)}\\ \neg \forall x & \in \mathbf{R}(x \ne 0 \rightarrow x \lt 0 \vee x \gt 0) & \textrm{(Brouwer 1949B)} \end{align*} \]

The actual arguments using these methods introduce no new logical phenomena as such—weak and strong counterexamples can also be given by other means. For the moment, we refer to the literature for further details: Brouwer 1949A, 1949B, 1954F; Heyting 1956: 117–120; Myhill 1966; Dummett 2000: 244–245. But we do note here one particular aspect of this method. It seems to introduce a further notion of negation, by accepting that, if it is known that the creating subject will never prove \(A\), then \(A\) is false. But this is actually no different from the notion of negation as impossibility. Heuristically, this can be seen as follows: given the freedom the creating subject has to construct whatever it can, the only way to show that there can be no moment at which the subject demonstrates \(A\) is to show that a demonstration of \(A\) itself is impossible. An actual justification of the principle is this: If the creating subject demonstrates a proposition \(A\), it does so at a particular moment \(n\); so, by contraposition, if it is contradictory that there exists a moment \(n\) at which the subject demonstrates \(A\), then \(A\) is contradictory.[11]

3.4 The Classification of Propositions

In Brouwer 1955, the four possible cases a proposition \(\alpha\) may be in at any particular moment are made explicit:

  1. \(\alpha\) has been proved to be true;
  2. \(\alpha\) has been proved to be false, i.e., absurd;
  3. \(\alpha\) has neither been proved to be true nor to be absurd, but an algorithm is known leading to a decision either that \(\alpha\) is true or that \(\alpha\) is absurd;
  4. \(\alpha\) has neither been proved to be true nor to be absurd, nor do we know an algorithm leading to the statement either that \(\alpha\) is true or that \(\alpha\) is absurd.

In a lecture from 1951, Brouwer lists only cases 1, 2, and 4 from the above list, adding that case 3 “obviously is reducible to the first and second cases” (Brouwer 1981A: 92). That remark emphasizes an important idealization permitted in intuitionistic mathematics: we may make the idealization that, once we have obtained a decision method for a specific proposition, we also know its outcome.

Brouwer also adds that a proposition for which case 4 holds may at some point pass to another case, either because we have in the meantime found a decision method, or because the objects involved in proposition \(\alpha\) in the meantime have acquired further properties that permit to make the decision (as may happen for propositions about choice sequences).

3.5 Brouwer’s View on the Formalist Program and Gödel’s Incompleteness Theorems

In 1908, Brouwer had shown that \(\neg \neg(A \vee \neg A)\); in 1923, when Hilbert’s program was in full swing, this result led Brouwer to say that “We need by no means despair of reaching this goal [of a consistency proof for formalized mathematics]”; see section 2.1 above for the full quotation. (At the time, Brouwer suspected that \(\neg \neg A \rightarrow A\) was weaker than PEM; Bernays quickly corrected this impression in a letter to Brouwer (Brouwer 1925E: 252n.4 [Mancosu 1998: 292n.4]).)

In 1928, he added to this the consistency of finite conjunctions of instances of PEM, and considered these results to “offer some encouragement” for the formalist project of a consistency proof (Brouwer 1928A2: 377 [Mancosu 1998: 43]).[12] The strongest statement based on these results he made at the end of the first Vienna lecture from 1928:

An appropriate mechanization of the language of this intuitionistically non-contradictory mathematics should therefore deliver precisely what the formalist school has set as its goal. (Brouwer 1929A: 164; translation mine)

But, for reasons explained above, such a consistency proof would have no mathematical value for Brouwer; and the best a classical mathematician can be said to be doing, according to the view Brouwer sketches, is to be giving relative consistency proofs.

Gödel’s incompleteness theorems showed that Hilbert’s Program, in its most ambitious form, cannot succeed. Brouwer’s assistant Hurewicz discussed the incompleteness theorem in a seminar (van Dalen 2005: 674n.7). There is no comment from Brouwer on Gödel’s first theorem in print; on the other hand, he clearly had the second theorem in mind when he wrote, in 1952, that

The hope originally fostered by the Old Formalists that mathematical science erected according to their principles would be crowned one day with a proof of non-contradictority, was never fulfilled, and, nowadays, in view of the results of certain investigations of the last few decades, has, I think, been relinquished. (Brouwer 1952B: 508)

Hao Wang reports:

In the spring of 1961 I visited Brouwer at his home. He discoursed widely on many subjects. Among other things he said that he did not think G’s incompleteness results are as important as Heyting’s formalization of intuitionistic reasoning, because to him G’s results are obvious (obviously true). (Wang 1987: 88)[13]

With respect to the first incompleteness theorem, Brouwer’s reaction is readily understandable. Already in his dissertation, he had noted that the totality of all possible mathematical constructions is “denumerably unfinished”; by this he meant that

we can never construct in a well-defined way more than a denumerable subset of it, but when we have constructed such a subset, we can immediately deduce from it, following some previously defined mathematical process, new elements which are counted to the original set. (Brouwer 1907: 148 [1975: 82])

And in one of the notebooks leading up to his dissertation, he stated that “The totality of mathematical theorems is, among other things, also a set which is denumerable but never finished”.[14]

Indeed, according to Carnap, it had been an argument of Brouwer’s that had stimulated Gödel in finding the first theorem. In a diary note for December 12, 1929, Carnap states that Gödel talked to him that day

about the inexhaustibility of mathematics (see separate sheet) He was stimulated to this idea by Brouwer’s Vienna lecture. Mathematics is not completely formalizable. He appears to be right. (Wang 1987: 84)

On the “separate sheet”, Carnap wrote down what Gödel had told him:

We admit as legitimate mathematics certain reflections on the grammar of a language that concerns the empirical. If one seeks to formalize such a mathematics, then with each formalization there are problems, which one can understand and express in ordinary language, but cannot express in the given formalized language. It follows (Brouwer) that mathematics is inexhaustible: one must always again draw afresh from the “fountain of intuition”. There is, therefore, no characteristica universalis for the whole mathematics, and no decision procedure for the whole mathematics. In each and every closed language there are only countably many expressions. The continuum appears only in “the whole of mathematics” … If we have only one language, and can only make “elucidations” about it, then these elucidations are inexhaustible, they always require some new intuition again. (As quoted, in translation, in Wang 1987: 50)

This record contains in particular elements from the second of Brouwer’s two lectures in Vienna, in which one finds the argument that Gödel refers to: on the one hand, the full continuum is given in a priori intuition, while on the other hand, it cannot be exhausted by a language with countably many expressions (Brouwer 1930A: 3, 6 [Mancosu 1998: 56, 58]).

The second incompleteness theorem, on the other hand, must have surprised Brouwer, given his optimism in the 1920s about the formalist school achieving its aim of proving the consistency of formalized classical mathematics (see the quotation at the beginning of this subsection).

In his final original published paper (1955), Brouwer was, in his own way, quite positive about the study of classical logic. After showing that various principles from the algebraic tradition in logic (e.g., Boole, Schröder) are intuitionistically contradictory, he continues:

Fortunately classical algebra of logic has its merits quite apart from the question of its applicability to mathematics. Not only as a formal image of the technique of common-sensical thinking has it reached a high degree of perfection, but also in itself, as an edifice of thought, it is a thing of exceptional harmony and beauty. Indeed, its successor, the sumptuous symbolic logic of the twentieth century which at present is continually raising the most captivating problems and making the most surprising and penetrating discoveries, likewise is for a great part cultivated for its own sake. (Brouwer 1955: 116)

3.6 Brouwer’s Logic and the Grundlagenstreit

Brouwer’s logic has played a role in the Grundlagenstreit (the Foundational Debate) only to the extent that this logic could be seen as a fragment of classical logic. Constructive logic in that sense was a success, and it became fundamental to Hilbert’s Program as well. On the other hand, phenomena specific to Brouwer’s full conception of logic, in particular the strong counterexamples, played no role in the Foundational Debate whatsoever. The main reason for this may be that, in their dependence on choice sequences, they use objects that are not acceptable in classical mathematics. (A more subtle matter is whether they are acceptable in Hilbert’s finitary mathematics. According to Bernays, Hilbert never took a position on choice sequences (Gödel 2003a: 279), and more generally never read Brouwer’s papers (van Dalen 2005: 637).[15]) In addition, Brouwer did not announce the existence of strong counterexamples in a loud or polemical way; and when in 1954 he finally did publish (in English) a paper with a polemical title—“An example of contradictority in classical theory of functions”—the Foundational Debate was, in the social sense, long over. Intuitionistic logic and mathematics had been widely accepted to the extent that they could be seen as the constructive part of classical mathematics, while the typically intuitionistic innovations were ignored. It is not surprising, then, that the presentation of the strong counterexamples in the 1950s did not at all lead to a reopening of the debate. For further discussion of this matter, see Hesseling 2003 and van Atten 2004a.

4. Early Partial Formalizations and Metamathematics

As Brouwer was more interested in developing pure mathematics than in developing logic, which for him was a form of applied mathematics, he never made an extensive study of the latter. In particular, he never made a systematic comparison of intuitionistic logic and classical logic as formalized, for example, in Principia Mathematica (Whitehead & Russell 1910) or by the Hilbert school (Hilbert 1923; Hilbert & Ackermann 1928). What motivated others to make such comparisons was the publication by Brouwer in international journals of weak counterexamples that showed how these also affected very general mathematical principles such as trichotomy for real numbers (see above, section 3.2).

Clearly, to make a systematic comparison possible, one needs a codification of intuitionistic logic in a formal system. On the intuitionistic view that cannot exist, as logic is as open-ended as the mathematics it depends on. But one may formalize fragments of intuitionistic logic. The relevant papers here are Kolmogorov 1925, Heyting 1928 (unpublished), Glivenko 1928, Glivenko 1929, and Heyting 1930.[16] But perhaps the first to give systematic thought to the matter was Paul Bernays. In a letter to Heyting of November 5, 1930, he wrote:

The lectures that Prof. Brouwer at the time held in Göttingen (for the first time) [1924 (van Dalen 2001: 305)], led me to the question how a Brouwerian propositional logic could be separated out, and I arrived at the result that this can be done by leaving out the single formula \(\neg \neg a \supset a\) (in your symbolism). I then also wrote to Prof. Brouwer [correcting Brouwer’s impression at the time that this formula is weaker than PEM]. (Troelstra 1990: 8)[17]

(Bernays’ correction was included, at the proof stage, in Brouwer’s paper (1925E: 252n.4 [Mancosu 1998: 292n.4]).) However, Bernays did not publish his idea for a Brouwerian logic. (Kolmogorov would publish the same idea in 1925; see below.)

In setting up a formal system to capture, albeit necessarily only in part, logic as it figures in Brouwer’s foundations, naturally some priorly obtained meaning explanation is needed to serve as the criterion for intuitionistic validity. Yet none of the papers by Kolmogorov, Heyting, and Glivenko just mentioned made an explicit contribution to the meaning explanation of intuitionistic logic. As we will see, the explanations as given in the papers (which is not necessarily all their respective authors had in mind) were too vague for that. It is perhaps not surprising, then, that the systems were not equivalent; notably, Kolmogorov rejected Ex Falso, while Heyting and Glivenko accepted it. We will now discuss these papers in turn.

4.1 Kolmogorov 1925

In 1925, Andrei Kolmogorov, at the age of 22, published the first (partial) formalization of intuitionistic logic, and also made an extensive comparison with formalized classical logic, in a paper called “On the principle of the excluded middle”. As van Dalen has suggested (Hesseling 2003: 237), Kolmogorov probably had come into contact with intuitionism through Alexandrov or Urysohn, who were close friends of Brouwer’s. Kolmogorov was in any case remarkably well-informed, citing even papers that had only appeared in the Dutch-language “Verhandelingen” of the Dutch Academy of Sciences (Brouwer 1918B, 1919A, 1921A).

The task Kolmogorov set himself in the paper is to explain why “the illegitimate use of the principle of the excluded middle” as revealed in Brouwer’s writings “has not yet led to contradictions and also why the very illegitimacy has often gone unnoticed” (van Heijenoort 1967: 416). In effect, as other passages make clear (van Heijenoort 1967: 429–430), the (unachieved) aim is to show that classical mathematics is translatable into intuitionistic mathematics, and thereby give a consistency proof of classical mathematics relative to intuitionistic mathematics.

The technical result established in the paper is: Classical propositional logic is interpretable in an intuitionistically acceptable fragment of it. The intuitionistic fragment, called \(\mathbf{B}\) (presumably for “Brouwer”) is:

\[ \begin{align} \tag{1} A & \rightarrow(B \rightarrow A)\\ \tag{2} (A \rightarrow(A \rightarrow B)) & \rightarrow (A \rightarrow B)\\ \tag{3} (A \rightarrow(B \rightarrow C)) & \rightarrow (B \rightarrow(A \rightarrow C))\\ \tag{4} (B \rightarrow C) & \rightarrow((A \rightarrow B) \rightarrow(A \rightarrow C))\\ \tag{5} (A \rightarrow B) & \rightarrow((A \rightarrow \neg B) \rightarrow \neg A)\\ \end{align} \]

The system \(\mathbf{H}\) (presumably for “Hilbert”) consists of \(\mathbf{B}\) and the additional axiom

\[\tag{6} \neg \neg A \rightarrow A \]

In both systems, the rules are modus ponens and substitution.

Kolmogorov then indicates and partially carries out a proof that \(\mathbf{H}\) is equivalent to the system for classical propositional logic presented by Hilbert in Hilbert 1923. Then Kolmogorov devises the following translation \(^*\):

\[ \begin{align*} A^* & = \neg \neg A & \textrm{for atomic } A\\ F(\phi_1, \phi_2 ,\ldots ,\phi_k)^* & = \neg \neg F(\phi_{1}^*, \phi_{2}^*,\ldots ,\phi_{k}^*) & \textrm{ for composed formulas} \end{align*} \]

and proves this interpretability result:

\[ \textrm{If } U \vdash_{\mathbf{H}} \phi \textrm{ then } U^* \vdash_{\mathbf{B}} \phi^* \]

where \(U\) is a set of axioms of \(\mathbf{H}\), and \(U^*\) the set of its translations (which Kolmogorov shows to be derivable in \(\mathbf{B})\).

Kolmogorov’s technical result anticipated Gödel’s and Gentzen’s “double negation translations” for arithmetic (see below), all the more so since he also made quite concrete suggestions how to treat predicate logic. As Hesseling (2003: 239) points out, however, to see Kolmogorov’s result as a translation into intuitionistic mathematics is slightly different from his own way of seeing it. Kolmogorov saw it as a translation into a domain of “pseudomathematics”; but although he did not explicitly identify that as part of intuitionistic mathematics, he could have done so.

Kolmogorov’s strategy to obtain a (fragment) of formalized intuitionistic logic was to start with a classical system and isolate an intuitionistically acceptable system from it. (Note that, although Kolmogorov refers to Principia Mathematica, he did not take it as his point of departure.) This might (roughly) be described as the method of crossing out, which is also what Heyting would do in 1928 (see below). Given the task Kolmogorov set himself, it is a natural approach. Kolmogorov’s criterion whether to keep an axiom was whether a proposition has an “intuitive foundation” or “possesses intuitive obviousness” (van Heijenoort 1967: 421, 422); on implication he said,

The meaning of the symbol \(A \rightarrow B\) is exhausted by the fact that, once convinced of the truth of \(A\), we have to accept the truth of \(B\) too. (van Heijenoort 1967: 420)

No more precise indications are given, so in that sense the paper did little to explain the meaning of intuitionistic logic.

Ex Falso was excluded from this fragment: Kolmogorov said that, just like PEM, Ex Falso “has no intuitive foundation” (van Heijenoort 1967: 419). In particular, he says that Ex Falso is unacceptable for the reason that it asserts something about the consequences of something impossible (van Heijenoort 1967: 421). Note that that is a very strong rejection: it not only rules out Ex Falso in its full generality, but also specific instances such as “If 3.15 is an initial segment of \(\pi\), then 3.1 is an initial segment of \(\pi\)”. It also indicates an incoherence in Kolmogorov’s position: one cannot at the same time accept \(A \rightarrow (B \rightarrow A)\) as an axiom and deny that anything can be asserted about the consequences of an impossible \(B\).

As van Dalen notes, it is not known whether Kolmogorov sent his paper to Brouwer (van Dalen 2005: 555). The contents of the paper seem to have remained largely unknown outside the Soviet Union for years. Glivenko mentioned the paper in a letter to Heyting of October 13, 1928, as did Kolmogorov in an undated letter to Heyting of 1933 or later (Troelstra 1990: 16); but in Heyting 1934 it is, unlike Kolmogorov’s later paper from 1932, neither discussed nor included in the bibliography. The volume of the Jahrbuch über die Fortschritte der Mathematik covering 1925, which included a very short notice on Kolmogorov 1925 by V. Smirnov (Leningrad), wasn’t actually published until 1932 (Smirnov 1925).

4.2 Heyting 1928

While Kolmogorov’s work remained unknown in the West, an independent initiative towards the formalization of intuitionistic logic and mathematics was taken in 1927, when the Dutch Mathematical Society chose to pose the following problem for its annual contest:

By its very nature, Brouwer’s set theory cannot be identified with the conclusions formally derivable in a certain pasigraphic system [i.e., universal notation system]. Nevertheless certain regularities may be observed in the language which Brouwer uses to give expression to his mathematical intuition; these regularities may be codified in a formal mathematical system. It is asked to

  1. construct such a system and to indicate its deviations from Brouwer’s theories;
  2. to investigate whether from the system to be constructed a dual system may be obtained by (formally) interchanging the principium tertii exclusi and the principium contradictionis. (Troelstra 1990: 4)

The question had been formulated by Brouwer’s friend, colleague, and former teacher Gerrit Mannoury, who asked Brouwer’s opinion on it beforehand in a letter (Brouwer was in Berlin);[18] unfortunately, no reply from Brouwer has been found, but the final formulation was the same as in Mannoury’s letter.

Brouwer’s former student Arend Heyting, who had graduated (cum laude) in 1925 with a dissertation on intuitionistic projective geometry, wrote what turned out to be the one submission (Hesseling 2003: 274). The original manuscript seems no longer to exist, but it is known that its telling motto was “Stones for bread”.[19] In 1928, the jury crowned Heyting’s work,[20] stating that it was “a formalization carried out in a most knowledgeable way and with admirable perseverance” (Hesseling 2003: 274; translation modified).

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).

Since the original manuscript seems not to have survived, a discussion of Heyting’s work must take the revised and published version from 1930 as its point of departure; see below.

Heyting sent his manuscript to Brouwer, who replied in a letter of July 17, 1928, that he had found it “extraordinarily interesting”, and continued:

By now I have already begun to appreciate your work so much, that I should like to request that you revise it in German for the Mathematische Annalen (preferably somewhat extended rather than shortened).[21]

Interestingly, Brouwer also suggested (with an eye on the formalization of the theory of choice sequences)

And, with an eye on §13, perhaps also the notion of “law” can be formalized.

It seems, however, that Heyting made no effort in that direction.

Heyting’s paper would indeed be published soon after, in 1930; not in the Mathematische Annalen, as Brouwer by then was no longer on its editorial board, but in the proceedings of the Prussian Academy of Sciences. However, Heyting’s work became known already before its publication. Heyting mentioned it in correspondence with Glivenko in 1928 (see below), Tarski and Łukasiewicz talked about it to Bernays at the Bologna conference in 1928, and Church mentioned it in a letter to Errera in 1929 (Hesseling 2003: 274).

4.3 Glivenko 1928 and 1929

In reaction to Barzin and Errera, who had argued that Brouwer’s logic was three-valued and moreover that this led to it being inconsistent, Valerii Glivenko[22] in 1928 set out to prove them wrong by formal means. He gave the following list of axioms for intuitionistic propositional logic:

\[ \begin{align} \tag{1} p &\rightarrow p\\ \tag{2} (p \rightarrow q) &\rightarrow((q \rightarrow r) \rightarrow(p \rightarrow r))\\ \tag{3} (p \wedge q) &\rightarrow p\\ \tag{4} (p \wedge q) &\rightarrow q\\ \tag{5} (r \rightarrow p) &\rightarrow((r \rightarrow q) \rightarrow(r \rightarrow(p \wedge q)))\\ \tag{6} p &\rightarrow(p \vee q)\\ \tag{7} q &\rightarrow(p \vee q)\\ \tag{8} \label{GlivAxiom8} (p \rightarrow r) &\rightarrow ((q \rightarrow r) \rightarrow((p \vee q) \rightarrow r))\\ \tag{9} (p \rightarrow q) &\rightarrow((p \rightarrow \neg q) \rightarrow \neg p)\\ \end{align} \]

From these axioms, he then proved

\[ \begin{align} \tag{1} \neg \neg(p \vee \neg p)\\ \tag{2} \neg \neg \neg p & \rightarrow \neg p\\ \tag{3} ((\neg p \vee p) \rightarrow \neg q) & \rightarrow \neg q\\ \end{align} \]

The first two had already informally been argued for by Brouwer (1908C, 1925E); the third was new. Now suppose that in intuitionistic logic, a proposition may be true \((p\) holds), false \((\neg p\) holds), or have a third truth value \((p'\) holds). Clearly, \(p \rightarrow \neg p'\) and \(\neg p \rightarrow \neg p'\), and therefore \((\neg p \vee p) \rightarrow \neg p'\); but then, by the third of the lemmata above and axiom \ref{GlivAxiom8} in the list, \(\neg p'\). As \(p\) is arbitrary, this means no proposition has the third truth value. (In 1932, Gödel would show that, more generally, intuitionistic propositional logic is no \(n\)-valued logic for any natural number \(n\); see section 4.5.1 below.)

Like Kolmogorov in 1925 and, as we will see, Heyting in 1930, Glivenko provided no detailed explanation of the intuitionistic validity of these axioms.

Glivenko immediately continued this line of work with a second short paper, Glivenko 1929, in which he showed, for a richer system of intuitionistic propositional logic:

  1. If \(p\) is provable in classical propositional logic, then \(\neg \neg p\) is provable in intuitionistic propositional logic;
  2. If \(\neg p\) is provable in classical propositional logic, then it is also provable in intuitionistic propositional logic.

The first theorem is not a translation in the usual sense (as Kolmogorov’s is), as it does not translate subformulas of \(p\); but it is strong enough to show that the classical and intuitionistic systems in question are equiconsistent.

The system of intuitionistic propositional logic is richer than in Glivenko’s previous paper, because to its axioms have now been added the following four:

\[ \begin{align} \tag{A} (p \rightarrow(q \rightarrow r)) & \rightarrow (q \rightarrow(p \rightarrow r))\\ \tag{B} (p \rightarrow(p \rightarrow r)) & \rightarrow (p \rightarrow r)\\ \tag{C} p & \rightarrow(q \rightarrow p)\\ \tag{D} \neg q & \rightarrow(q \rightarrow p)\\ \end{align} \]

Interestingly, Glivenko mentions in his paper that “It is Mr. A. Heyting who first made me see the appropriateness of the two axioms C and D in the Brouwerian logic” (Mancosu 1998: 304–305n.3). The two had come into correspondence when, upon the publication of Glivenko 1928, Heyting sent Glivenko a letter (Troelstra 1990: 11). Kolmogorov in 1925 had explicitly rejected Ex Falso for having no “intuitive foundation”. From Glivenko’s letter to Heyting of October 13, 1928, we know that Glivenko was aware of this (Troelstra 1990: 12). In his paper, however, which he finished later, he does not mention Kolmogorov at all. Instead, he makes the remark on Heyting just quoted and then justifies D by saying that it is a consequence of the principle \((p \vee \neg q) \rightarrow (q \rightarrow p)\), the admissibility of which he considers “quite evident”.[23] From a Brouwerian point of view, however, the principle is as objectionable as Ex Falso.[24] It is worth noting that, when Heyting gave his justification for Ex Falso in Heyting 1956: 102, he did not appeal to the principle Glivenko had used (nor did Kolmogorov in 1932). From Glivenko’s letter of October 18, 1928, one gets the impression that this principle had not been the argument Heyting had actually given to convince him:

I am now convinced by your reasons that intuitionistic mathematics need not reject that axiom, so that all considerations against that axiom might lead beyond the limits of our present subject matter. (Troelstra 1990: 12; translation mine)

Heyting had informed Glivenko of the planned publication of his (revised and translated) prize essay from 1928 in the Mathematische Annalen. On October 30, 1928, Glivenko asked Heyting if he also was going to include the result that if \(p\) is provable in classical propositional logic, then \(\neg\neg p\) is provable in intuitionistic propositional logic; for if he would, then there would be no point for Glivenko in publishing his own manuscript. Two weeks later, Glivenko had changed his mind, writing to Heyting on November 13 that, even though this result “is but an almost trivial remark”, “its rigorous demonstration is a bit long” and he wants to publish it independently of Heyting’s paper. Indeed, Glivenko’s paper was published first, and in it the publication of Heyting’s formalization was announced; and when Heyting published his paper in 1930, he included a reference to Glivenko 1929, stating its two theorems, and he also acknowledged the use of results from Glivenko 1928. Heyting’s note “On intuitionistic logic”, also from 1930, begins with a reference to Glivenko’s “two excellent articles” from 1928 and 1929.

4.4 Heyting 1930

Heyting’s (partial) formalization of intuitionistic logic and mathematics in Heyting 1930, Heyting 1930A, and Heyting 1930B, is perhaps, as far as the parts on logic are concerned, the most influential intuitionistic publication ever, together with his book Intuitionism: An Introduction from 1956.

Heyting’s formalization comprised intuitionistic propositional and predicate logic, arithmetic, and analysis, all together in one big system (with only variables for arbitrary objects). The part concerned with analysis was, not only in its intended interpretation (involving choice sequences) but also formally, no subsystem of its classical counterpart; this explains why it sparked no general interest at the time. (A consequence we noted above is that Brouwer’s strong counterexamples never affected the debate.) Therefore this part of Heyting’s formalization was left out of consideration by the other participants in the Foundational Debate.[25] This was different for the parts concerned with logic and arithmetic. Formally speaking and disregarding their intended interpretations, from these one could distill subsystems of their classical counterparts, from which only PEM (or double negation elimination) is missing. No doubt this encouraged many to accord to these systems a definitive character, which, as Heyting had remarked at the beginning of his paper, on the intuitionistic conception of logic they cannot have:

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 1930: 42 [Mancosu 1998: 311])

However, Heyting himself, however, wrote some five decades later,

I regret that my name is known to-day mainly in connection with these papers [Heyting 1930, 1930A, 1930B], which were very imperfect and contained many mistakes. They 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 1978: 15)

The fear that the attention might be thus diverted had indeed been expressed in the first of the three papers themselves:

Section 4 [on negation] departs substantially from classical logic. Here I could not avoid giving the impression that the differences that come to the fore in this section constitute the most important point of conflict between intuitionists and formalists (a claim that is already refuted by the remark made at the beginning [quoted above]); this impression arises because the formalism is unfit to express the more fundamental points of conflict. (Heyting 1930: 44 [Mancosu 1998: 313])

For the full system, including predicate logic and analysis, the reader is referred to Heyting’s original papers. Heyting’s axioms for intuitionistic propositional logic were:

\[ \begin{align} \tag{1} a &\rightarrow(a \wedge a)\\ \tag{2} (a \wedge b) &\rightarrow(b \wedge a)\\ \tag{3} (a \rightarrow b) &\rightarrow((a \wedge c)\rightarrow(b \wedge c))\\ \tag{4} ((a \rightarrow b) \wedge(b \rightarrow c)) &\rightarrow(a \rightarrow c)\\ \tag{5} \label{HeytingAxiom5} b &\rightarrow(a \rightarrow b)\\ \tag{6} (a \wedge(a \rightarrow b)) &\rightarrow b\\ \tag{7} a &\rightarrow(a \vee b)\\ \tag{8} (a \vee b) &\rightarrow(b \vee a)\\ \tag{9} ((a \rightarrow c) \wedge(b \rightarrow c)) &\rightarrow((a \vee b) \rightarrow c)\\ \tag{10} \label{HeytingAxiom10} \neg a &\rightarrow(a \rightarrow b)\\ \tag{11} ((a \rightarrow b) \wedge(a \rightarrow \neg b)) &\rightarrow \neg a\\ \end{align} \]

In a letter to Oskar Becker, Heyting described the approach used to obtain these axioms, as well as those for predicate logic, as follows:

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. (Heyting to Becker, September 23, 1933 (draft) [van Atten 2005: 129], original italics, translation mine)

As Heyting emphasizes here, the theorems of Principia Mathematica also had to be looked at, for a theorem might be intuitionistically acceptable even when a classical proof given for it is not.[26] It is worth noting that Heyting used this method of crossing out, as also Kolmogorov had, instead of determining the logic directly from general considerations on mathematical constructions in Brouwer’s sense. (To some extent, Kreisel tried to do that systematically in the 1960s.) In his dissertation on intuitionistic axiomatization of projective geometry, Heyting had already gained experience with developing an intuitionistic system by taking a classical axiomatic system as guideline and then adjusting it.[27]

In Mints 2006 (section 2) it has been observed that Russell 1903 (section 18) anticipated intuitionistic propositional logic by identifying Peirce’s law and using it to separate out the principles that imply PEM. It seems that Heyting did not realize this at the time; among the references given in Heyting 1930, Russell’s book does not appear.

Heyting shows the independence of his axioms using a method given by Bernays (1926); this use of a non-intended interpretation for metamathematical purposes Heyting accepted without hesitation, but he remarked that such metamathematics is “less important for us [intuitionists]” than the approach where all formulas are considered to be meaningful propositions (Heyting 1930: 43 [Mancosu 1998: 312]).

Heyting states Glivenko’s two theorems from 1929, without giving proofs.

Unlike Kolmogorov, but like Glivenko (who had been convinced by Heyting), Heyting accepted Ex Falso (axiom \ref{HeytingAxiom10} above). He was somewhat more elaborate on this point than they had been:

The formula \(a \rightarrow b\) generally means: “If \(a\) is correct, then \(b\) is correct too”. This proposition is meaningful if \(a\) and \(b\) are constant propositions about whose correctness nothing need be known … The case if conceivable that after the statement \(a \rightarrow b\) has been proved in the sense specified, it turns out that \(b\) is always correct. Once accepted, the formula \(a \rightarrow b\) then has to remain correct; that is, we must attribute a meaning to the sign \(\rightarrow\) such that \(a \rightarrow b\) still holds. The same can be remarked in the case where it later turns out that \(a\) is always false. For these reasons, the formulas [\ref{HeytingAxiom5}] and [\ref{HeytingAxiom10}] are accepted. (Heyting 1930: 44 [Mancosu 1998: 313])

The argument is, however, incomplete. It is uncontroversial that, once \(a \rightarrow b\) has been proved, it should remain so when afterward \(\neg a\) is proved. But why should \(a \rightarrow b\), if it has not yet been proved, become provable just by establishing \(\neg a\)? (Johansson asked this in a letter to Heyting in 1935;[28] see section 6.1 below). Clearly, then, further work needed to be done on the explanation of intuitionistic logic.

4.5 The Turn to Heyting’s Formalized Logic and Arithmetic

After the publication of Heyting’s series of papers, three roads could be taken, and indeed were (cf. Posy 1992):

  1. to explicate and develop the meaning explanation that had given rise to Heyting’s system;
  2. to engage in metamathematical study of the formal systems distilled from Heyting’s system;
  3. to find alternative motivations for (parts of) Heyting’s system that are independent from the intuitionists’, yet also in some sense constructive (e.g., Lorenzen’s dialogue semantics)

By and large, these three roads lead to very different areas, with correspondingly divergent histories, of which no unified account can be expected. (However, in the Dialectica Interpretation, as proposed and understood by Gödel (1958, 1970, 1972), they came close to one another.) In accordance with the main theme of the present account, in the remaining sections we will be concerned with the historical development of the meaning explanations. But a number of early highlights of the formal turn must be mentioned here.

4.5.1 Some early results

  1. Intuitionistic propositional logic is not a finitely valued logic. Gödel (1932) showed that Heyting’s system for intuitionistic propositional logic cannot be conceived of as a finitely many-valued logic. Apparently unbeknown to Gödel, this confirmed a conjecture of Oskar Becker (1927: 775–777). Gödel’s result, which came soon after his incompleteness theorem, led Heyting to write to him,

    It is as if you had a malicious pleasure in showing the purposelessness of others’ investigations … In the sense of economy of thought this work is certainly useful, and in addition to that comes the particular beauty of your short proof. [Heyting to Gödel, letter dated 24 and 26 November 1932. (Gödel 2003a: 67)

  2. Peano Arithmetic is translatable into Heyting Arithmetic. A seminal theorem was obtained independently by Gödel (1933e) and by Gentzen (withdrawn upon learning of Gödel’s paper): There is a translation \('\) from PA to HA such that

    \[\textbf{PA} \vdash A \Leftrightarrow \textbf{HA} \vdash A'\]

    (Gödel and Gentzen actually used Herbrand’s axioms for the natural numbers (Herbrand 1931), but that is immaterial here.) The same proofs serve to show that the same result holds for pure predicate logic. This completes and generalizes Kolmogorov’s result from 1925, which at the time was known to neither Gentzen nor Gödel (Gödel does cite Glivenko 1929). Gödel concluded that

    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 1933e: 37 [1986: 295])

    Heyting replied that “for the intuitionist, the interpretation is what is essential” (Heyting 1934: 18; translation mine). Later Gödel became, as Kreisel put it, “supersensitive about differences in meaning” (Kreisel 1987a: 82). The Gödel-Gentzen translation had an immediate application to the foundational debate, in which besides the notion of existence the status of PEM had been the main issue (Hesseling 2003): the embedding of PA into HA shows that PA is consistent if and only if HA is. As Gödel observed,

    The above considerations, of course, provide an intuitionistic consistency proof for classical arithmetic and number theory. This proof, however, is not “finitary” in the sense in which Herbrand, following Hilbert, used the term. (Gödel 1933e: 37–38 [1986: 295])[29]

    Indeed, according to Bernays (1967: 502), it was this fact that made it clear that intuitionism is stronger than Hilbert’s finitism.

  3. Interpreting intuitionistic logic in a classical provability logic, Gödel (1933f) presented a mapping \('\) of intuitionistic propositional logic PC to classical modal logic S4 such that

    \[ \textbf{IPC} \vdash A \Rightarrow \textbf{S4} \vdash A' \]

    For more details on this result, see the section Gödel’s Work in Intuitionistic Logic and Arithmetic of Kennedy 2007, as well as Artemov 2001.

    As pointed out by Troelstra (Gödel 1986: 299), at the time Gödel certainly knew the content of Heyting 1931. He had attended the Königsberg conference (where Heyting had presented that paper) and had published a review (Gödel 1932f) of the printed version. In that paper, Heyting had introduced a provability operator, but considered it redundant given the intuitionistic conception of truth as provability (see below, section 5.1).[30]

  4. Consider the following two properties:
    • the Disjunction Property (DP): if \(\vdash A \vee B\), then \(\vdash A\) or \(\vdash B\);
    • the Explicit Definability property (EP): if \(\vdash \exists x P(x)\), then \(\vdash P(t)\) for some term \(t\)
    DP for intuitionistic propositional calculus was stated by Gödel (1932: 66 [1986: 225]), who did not give a proof. A proof was given for intuitionistic predicate logic by Gentzen (1934). As Troelstra and van Dalen (1988: 175) observe, the same method (cut-elimination) yields ED for intuitionistic predicate calculus. For Heyting Arithmetic, see Kleene 1945 (section 8) and Kleene 1952 (theorem 62b).
  5. The intuitionistic connectives are not interdefinable: none of \(\rightarrow , \wedge , \vee , \neg\) can be defined in terms of the others. Heyting had stated this in Heyting 1930: 44 [Mancosu 1998: 312], but without giving a proof. A proof was published by Wajsberg (1938) and (independently and by different methods) by McKinsey (1939).

4.5.2 Mathematical interpretations and model-theoretic semantics

Various mathematical interpretations (in the sense explained in section 1.2) of formalized intuitionistic logic and arithmetic have been proposed. Above we saw Gödel’s translation of intuitionistic propositional logic into the classical modal logic S4 from 1933; further examples are Kleene’s realizability (Kleene 1945), and Gödel’s Dialectica Interpretation (Gödel 1958, 1970, 1972).

Such mathematical interpretations are not meaning explanations. There are two arguments. The first is that, in a context where formal systems are arithmetized, interpretability results are established wholly within mathematics (e.g., Joosten 2004). But then no contact at all is made with the concepts that figure in meaning explanations, which have to do with our cognitive capacities, such as those of effecting mathematical constructions or those of understanding, learning, and using a language. The second, more general argument is due to Sundholm (1983: 159). Here we consider \(A\) and its interpretation \(A'\) not as syntactical objects but as meaningful propositions. Then the argument is that, by whatever means one correlates a mathematical proposition \(A'\) to a mathematical proposition \(A\), it makes sense to ask whether the propositions \(A\) and \(A'\) are equivalent. On the other hand, it does not make sense to ask whether the proposition \(A\) is equivalent to a specification of what one has to know in order to understand \(A\) and use it correctly; for example, that specification remains the same whether \(A\) is true, false, or undecided. But then \(A'\) cannot be a meaning explanation of \(A\).

It would therefore be a mistake to see in mathematical interpretations of intuitionistic systems ways to make the Proof Interpretation “rigorous” or “precise”. The difference is not one of degree but of kind.[31] The point is general, and it makes no difference if the interpreting theory \(V\) is intuitionistic.[32] On the other hand, it is not at all ruled out that for an interpreting theory \(V\) itself an explanation can be given that is arguably superior to the Proof Interpretation in some respect; this was Gödel’s philosophical aim for his Dialectica Interpretation.

A related point can be made about model-theoretic semantics for a(ny) logic (Dummett 1973: 293–294): these map formulas to mathematical objects, without there being an intrinsic connection between those objects and the concepts related to our understanding and use of a language. By itself, therefore, such a semantics does not contribute to a meaning explanation. (The first argument on mathematical interpretations, above, is essentially the same as this one.) But for metamathematical purposes, such model-theoretic semantics have proved extremely valuable. Note that Heyting (1930) used model-theoretic semantics to show the independence of his axioms for propositional logic. A wide variety of model-theoretic semantics for intuitionistic systems has been developed since, beginning with the topological ones of Stone (1937) and Tarski (1938). Of the remaining ones, among the best known are Beth models (Beth 1956), Kripke models (Kripke 1965), and topos models. For Kripke models, see the section Kripke semantics for intuitionistic logic of Moschovakis 2007; for other models and further references, see Kleene and Vesley 1965: 6 and Artemov 2001.

5. The Proof Interpretation Made Explicit

5.1 Heyting 1930, 1931

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.

Heyting began to expound on the meaning of the connectives in print in two papers written in 1930. The first, Heyting 1930C, was published that same year, the second, the text of his lecture at Königsberg in September 1930, was published the next year (Heyting 1931).

The first paper was a reaction to Barzin and Errera’s claim that Brouwer’s logic is three-valued (Barzin & Errera 1927). The relevant points for the explanation of the meaning of the connectives in Heyting’s paper are the following. First, an explanation is given of assertion:

Here, then, is the Brouwerian assertion of \(p\): It is known how to prove p. We will denote this by \(\vdash p\). The words “to prove” must be taken in the sense of “to prove by construction”. [original italics](Heyting 1930C: 959 [Mancosu 1998: 307])

And then of intuitionistic negation:

\(\vdash \neg p\) will mean: “It is known how to reduce \(p\) to a contradiction”. (Heyting 1930C: 960 [Mancosu 1998: 307])

Heyting goes on to explain that, although on these explanations there is a third case beside \(\vdash p\) and \(\vdash \neg p\), namely the case where one knows neither how to prove \(p\) nor how to refute it, this does not mean there is a third truth value:

This case could be denoted by \(p'\), but it must be realized that \(p'\) will hardly ever be a definitive statement, since it is necessary to take into account the possibility that the proof of either \(p\) or \(\neg p\) might one day succeed. If one does not wish to risk having to retract what one has said, in the case \(p'\) one should not state anything at all. (Heyting 1930C: 960 [Mancosu 1998: 307])

This refutes the contention of Barzin and Errera. Note that these points are all in Brouwer’s writings, too. Indeed, Heyting (1932: 121) objects to Barzin and Errera’s term “Heyting’s logic”, saying that “all the fundamental ideas of that logic come from Brouwer” (translation mine). But Heyting’s papers will have found a wider audience than Brouwer’s. Brouwer, in turn, was very positive about the paper Heyting 1930C, and wrote to the editor of the journal in which it appeared (Brouwer to de Donder, October 9, 1930):

While preparing a note on intuitionism for the Bulletin de l’Académie Royale de Belgique,[33] I was pleasantly surprised to see the publication of a note by my student Mr. Heyting, which elucidates in a magisterial manner the points that I wanted to shed light upon myself. I believe that after Heyting’s note little remains to be said. (van Dalen 2005: 676)

Heyting also proposes a provability operator +, where \(+p\) means “\(p\) is provable”. The distinction between \(p\) and \(+p\) is relevant if one believes that (at least some) propositions are true or false independently of our mathematical activity. In that case one can go on and develop a provability logic, as for example Gödel did (see section 4.5.1 above). That is not the intuitionistic conception, and Heyting remarks that, if the fulfillment of \(p\) requires a construction, then there is no difference between \(p\) and \(+p\). He adds that, on the intuitionistic explanation of negation, there is indeed no difference between \(\neg p\) and \(+\neg p\), as a proof of \(\neg p\) is defined as a construction that reduces \(p\) to a contradiction. But Heyting does not generalize this remark to all of intuitionistic logic. The final section of the paper is a further discussion of the logic of the provability operator, in particular its interaction with negation (e.g., \(\vdash \neg +p\) is the assertion that \(p\) is unprovable). But Heyting ends by saying that, as the intuitionists’ task is the reconstruction of all mathematics, while at the same time no examples of propositions have been found so far for which this provability operator would be necessary to express their status (e.g., to express absolute undecidability), it cannot be asked of intuitionists that they develop this logic (Heyting 1930C: 963 [Mancosu 1998: 309–310])

The Königsberg lecture, given in 1930 and published in 1931, specifies the meanings of \(p, \neg p\), and \(p \vee q\). This time Heyting makes an explicit connection to phenomenology:

We here distinguish between propositions [Aussagen] and assertions [Sätze]. An assertion is the affirmation of a proposition. A mathematical proposition expresses a certain expectation. For example, the proposition, “Euler’s constant \(C\) is rational”, expresses the expectation that we could find two integers \(a\) and \(b\) such that \(C = a / b\). Perhaps the word “intention”, coined by the phenomenologists, expresses even better what is meant here … The affirmation of a proposition means the fulfillment of an intention. (Heyting 1931: 113 [Benacerraf & Putnam 1983: 58–59])

Compared to the earlier paper written in 1930, the point about the provability operator is amplified:

The distinction between \(p\) and \(+p\) vanishes as soon a construction is intended in \(p\) itself, for the possibility of a construction can be proved only by its actual execution. If we limit ourselves to those propositions which require a construction, the logical function of provability does not arise at all. We can impose this restriction by treating only propositions of the form “\(p\) is provable”, or, to put it another way, by regarding every intention as having the intention of a construction for its fulfillment added to it. It is in this sense that intuitionistic logic, insofar as it has been developed up to now without using the function +, must be understood. (Heyting 1931: 115 [Benacerraf & Putnam 1983: 60; translation modified])

The explanation of disjunction in the Königsberg lecture is:

“\(p \vee q\)” signifies that intention which is fulfilled if and only if at least one of the intentions \(p\) and \(q\) is fulfilled. (Heyting 1931: 114 [Benacerraf & Putnam 1983: 59])

And of negation:

Becker, following Husserl, has described its meaning very clearly. For him negation is something thoroughly positive, viz., the intention of a contradiction contained in the original intention. The proposition “\(C\) is not rational”, therefore, signifies the expectation that one can derive a contradiction from the assumption [Annahme] that \(C\) is rational. It is important to note that the negation of a proposition always refers to a proof procedure which leads to the contradiction, even if the original proposition mentions no proof procedure. (Heyting 1931: 113 [Benacerraf & Putnam 1983: 59])

Heyting pointed out that these explanations for disjunction and negation, taken together, are an immediate argument against the acceptability of PEM, for which a general method would be needed that, applied to any given proposition \(p\), produces either a proof of \(p\) or a proof of \(\neg p\). What Heyting did not do here was to generalize this explanation of negation to one for implication. Also, note that the procedure does not operate on proofs of \(p\), but starts from merely the assumption that \(p\), which in general gives less information. Both points were taken care of shortly afterward. In a letter to Freudenthal dated October 25, 1930, shortly after the Königsberg lecture, Heyting wrote:

From your remarks it has become clear to me that the simple explanation of \(a \rightarrow b\) by “When I think \(a\), I must think \(b\)” is untenable; this idea is in any case too indeterminate to be able to serve as the foundation for a logic. But also your formulation: “When \(a\) has been proved, so has \(b\)”, is not wholly satisfactory to me; when I ask myself what you may mean by that, I believe that also \(a \rightarrow b\), like the negation, should refer to a proof procedure: “I possess a construction that derives from every proof of \(a\) a proof of \(b\)”. In the following, I will keep to this interpretation. There is therefore no difference between \(a \rightarrow b\) and \(+a \rightarrow +b\). (Troelstra 1983: 206–207; translation mine)

This explanation of implication, which is the one that became standard, would be introduced in print only in Heyting 1934: 14; in his paper 1932C, Heyting used the explanation given in Kolmogorov 1932 instead (see below).

Neither of these two papers by Heyting contained an argument for the validity of Ex Falso.

5.2 Influences on Heyting

A number of influences (or possible influences) on Heyting’s arriving at the Proof Interpretation can be suggested. The following are publications Heyting had all seen by 1927, for he refers to them in his dissertation (1925: 93–94):

  • Brouwer 1907 (Ch. 3) and Brouwer 1908C, which forcefully made the point that intuitionistic logic is concerned with the preservation of constructibility;
  • Brouwer’s proof of the bar theorem from 1924, handed in on March 29, 1924 (Brouwer 1924D1: 189 [Mancosu 1998: 36]), and perhaps also the later version from 1927, of which the manuscript was handed in on April 28, 1926 (Brouwer 1927B: 75 [van Heijenoort 1967: 446]); both show how to operate mathematically on demonstrations as objects.
  • Weyl 1921, where universal and existential theorems are considered to be not genuine judgements at all, but “Urteilsanweisungen” (judgement instructions) and “Urteilsabstrakte” (judgement abstracts), thus emphasizing that such theorems for their justification need to be backed up by a construction method. Brouwer, in a note on Weyl’s paper, agreed, saying “This is only a matter of name and certainly does not reflect any lacking insight on my part” (Mancosu 1998: 122).

A further likely influence is Brouwer’s unpublished elucidation of the virtual ordering axioms (see section 3.1.3 above). Dirk van Dalen (personal communication) suspects that, although Heyting was probably not present at this lecture course, he heard Brouwer make a similar comment on another occasion (for example during the years 1922–1925, when Heyting was working on his dissertation under Brouwer, for that work also considers intuitionistic orderings).

5.3 Kolmogorov 1932 and Heyting 1934

In 1932, Kolmogorov presented a logic of problems and their solutions, and pointed out that the logic this explanation validates is formally equivalent to the intuitionistic propositional and predicate logic presented by Heyting in 1930. Moreover, he suggests that this provides a better interpretation than Heyting’s.

Kolmogorov’s idea is this:

If \(a\) and \(b\) are two problems, then \(a \wedge b\) designates the problem “to solve both problems \(a\) and \(b\)”, while \(a \vee b\) designates the problem “to solve at least one of the problems \(a\) and \(b\)”. Furthermore, \(a \supset b\) is the problem “to solve \(b\) provided that the solution for \(a\) is given” or, equivalently, “to reduce the solution of \(b\) to the solution of \(a\)” \(\ldots \neg a\) designates the problem “to obtain a contradiction provided that the solution of \(a\) is given” \(\ldots(x)a(x)\) stands in general for the problem “to give a general method for the solution of \(a(x)\) for every single value of \(x\)”. (Kolmogorov 1932: 59 [Mancosu 1998: 329])

He then lists Heyting’s axioms for propositional logic (with Heyting’s numbering) and, by discussing an example, makes it clear that these all hold when interpreted as statements about problems and their solutions. He also points out that \(a \vee \neg a\) is the problem

to give a general method that allows, for every problem \(a\), either to find a solution for \(a\), or to infer a contradiction from the existence of a solution for \(a\)!

In particular, if the problem \(a\) consists in the proof of a proposition, then one must possess a general method either to prove or to reduce to a contradiction any proposition. (Kolmogorov 1932: 63 [Mancosu 1998: 332]).

In the second part of his paper, Kolmogorov argues that, given the epistemological tenets of intuitionism,

intuitionistic logic should be replaced by the calculus of problems, for its objects are in reality not theoretical propositions but rather problems. (Kolmogorov 1932: 58 [Mancosu 1998: 328])

That he considers his interpretation an alternative to Heyting’s, and a preferable one, is again emphasized in a note added in proof:

This interpretation of intuitionistic logic is closely connected with the ideas Mr. Heyting has developed in the last volume of Erkenntnis 2, 1931: 106 [Heyting 1931]; yet in Heyting a clear distinction between propositions and problems is missing. (Kolmogorov 1932: 65 [Mancosu 1998: 334])

But it is not at all clear that Heyting would want to make that distinction. If the notion of proposition is understood in such a way that a proposition is true or false independently of our knowledge of this fact, then Heyting would readily agree with Kolmogorov that a proposition is different from a problem; but as soon as one adopts the view that propositions express intentions that are fulfilled (i.e., made true) or disappointed (made false) by our mathematical constructions, which is the view that Heyting actually held, then there would seem to be no essential difference between propositions and problems. Kolmogorov himself had already indicated that a problem may consist in finding the proof of a proposition; exploiting this, one can argue that the following two notions of proposition coincide:

  1. propositions express intentions towards constructions
  2. propositions pose problems which are solved by carrying out constructions

The basic idea is that a proposition in sense 1 gives rise to the problem of finding a construction that fulfills the expressed intention, and that a solution to a problem posed in a proposition in sense 2 also serves to fulfill the intention towards constructions that solve that problem; this is made fully explicit in a little argument due to Martin-Löf, given in detail in Sundholm 1983: 158–159.

In a letter to Heyting of October 12, 1931, Kolmogorov in effect agrees that the difference between Heyting and him is mainly a terminological matter (Troelstra 1990: 15).

Heyting later claimed that Kolmogorov’s meaning explanation and his own amounted to the same (Heyting 1958C: 107). By 1937, Kolmogorov seems to have come to believe the same, as in a review in the Zentralblatt of an exchange between Freudenthal and Heyting (discussed in section 6.1 below), he consistently speaks of “intention or problem” (Kolmogorov 1937). In that exchange itself, Freudenthal (1937: 114) had said that between Heyting’s and Kolmogorov’s explanations there was “no essential difference”. Finally, Oskar Becker, in a letter to Heyting of September 1934, had remarked that Heyting’s interpretation is a generalization of Kolmogorov’s, as a “problem” and its “solution” are special cases of an intention and its fulfillment. “Intuitionistic logic is therefore a ‘calculus of intentions’”.[34]

However, a complication for the identification of Heyting’s and Kolmogorov’s explanations of logic is introduced by Kolmogorov’s also accepting, in a particular case, solutions that do not consist in a carrying out a concrete construction. Kolmogorov said that “As soon as \(\neg a\) is solved, then the solution of \(a\) is impossible and the problem \(a \rightarrow b\) is without content” (Kolmogorov 1932: 62 [Mancosu 1998: 331]), and proposed that “The proof that a problem is without content [owing to an impossible assumption] will always be considered as its solution” (Kolmogorov 1932: 59: [Mancosu 1998: 329]). Taken together, this yields a justification of Ex Falso, \(\neg a \rightarrow(a \rightarrow b)\).

It seems not altogether unreasonable to extend the meaning of the term “solution” this way, for, just like a concrete solution, an impossibility proof also provides what might be called “epistemic closure”: like a concrete solution, it provides a completely convincing reason to stop working on a certain problem. (This kind of “higher-order” solution is also familiar from Hilbert’s Program, e.g., Hilbert 1900: 51.) Note that this justification of Ex Falso makes no attempt to describe a counterfactual mathematical construction process; thus, Kolmogorov’s justification from 1932 is not incompatible with the ground for his rejection of Ex Falso in 1925, namely, that one cannot constructively assert consequences of something impossible. Rather, the solution from 1932 introduces a stipulation to achieve completion of the logical theory for its own sake.

On the other hand, although Kolmogorov’s stipulation is neither unreasonable nor unmotivated, on Brouwer’s descriptive conception of logic there is of course no place for stipulation. For this reason, “Proof Interpretation” seems to be a more appropriate name for an explanation of Brouwerian logic than “BHK Interpretation”.

On Heyting’s explanation, however, a justification of Ex Falso parallel to Kolmogorov’s would seem to be impossible: while a problem may find a “higher-order” solution when it is shown that a solution is impossible, it makes no sense to say that an intention finds “higher-order” fulfillment when it is shown that it cannot be fulfilled. The notion of a solution seems to permit a reasonable extension that the notion of fulfillment does not. In his book from 1934, Heyting explains Ex Falso in Kolmogorov’s terms, not his own. After stating the axiom \(\neg a \supset (a \supset b)\), he says:

It is appropriate to interpret the notion of “reducing” in such a way, that the proof of the impossibility of solving \(a\) at the same time reduces the solution of any problem whatsoever to that of \(a\). (Heyting 1934: 15; translation mine)

Clearly there is a difference between Kolmogorov’s own explanation and Heyting’s explanation in Kolmogorov’s terms. Where Heyting says that a proof of \(\neg a\) establishes a reduction of the solution of any problem to that of \(a\), Kolmogorov had said that it established that the problem of reducing the solution of any problem to that of \(a\) has become without content. One has the impression that Heyting in his explanation of Ex Falso tries to approximate as closely as possible the explanation for ordinary implications in terms of a concrete constructive connection between antecedent and consequent; this is even clearer in the explanation he would give of Ex Falso in 1956 (see section 5.4 below). (Note that neither Heyting nor Kolmogorov ever justified Ex Falso by giving the traditional argument (based on the disjunctive syllogism) also stated in Glivenko’s paper from 1929; see section 4.3 above.)

More generally, the explanation of logic in Heyting 1934 is for the most part given Kolmogorov style, and not Heyting’s own in terms of intentions and their fulfillment. (The latter is only mentioned for its explanation of the implication (Heyting 1934: 14).) Perhaps the reason for this is that Heyting (1934: 14) agrees with Kolmogorov (1932: 58) that the interpretation in terms of problems and solutions provides a useful interpretation Heyting’s formal system also for non-intuitionists (while for intuitionists they come to the same thing). In his short note 1932C, titled “The application of intuitionistic logic to the definition of completeness of a logical calculus”, Heyting uses Kolmogorov’s interpretation instead of his own. Given the subject matter, that is what one might expect.

5.4 Heyting 1956

In his influential book Intuitionism. An introduction from 1956, Heyting explains the logical connectives as follows (97–98, 102):

  1. “A mathematical proposition \(p\) always demands a mathematical construction with certain given properties; it can be asserted as soon as such a construction has been carried out”.
  2. “\(p \wedge q\) can be asserted if and only if both \(p\) and \(q\) can be asserted”.
  3. “\(p \vee q\) can be asserted if and only if at least one of the propositions \(p\) and \(q\) can be asserted”.
  4. “\(\neg p\) can be asserted if and only if we possess a construction which from the supposition that a construction \(p\) were carried out, leads to a contradiction”.
  5. “The implication \(p \rightarrow q\) can be asserted, if and only if we possess a construction \(r\), which, joined to any construction proving \(p\) (supposing that the latter be effected), would automatically effect a construction proving \(q\)”.
  6. “\(\vdash(\forall x)p(x)\) means that \(p(x)\) is true for every \(x\) in \(Q\) [over which \(x\) ranges]; in other words, we possess a general method of construction which, if any element \(a\) of \(Q\) is chosen, yields by specialization the construction \(p(a)\)”.
  7. “\((\exists x)p(x)\) will be true if and only if an element \(a\) of \(Q\) for which \(p(a)\) is true has actually been constructed”.

Note that these explanations are not in terms of proof conditions, but of assertion conditions. This may make a difference in particular for the explanation of implication, where, instead of only the information under what condition something counts as a proof of \(p\), we now can also take into consideration that, by hypothesis, a concrete construction for \(p\) has been effected. As we saw in section 3.1.2, the possibility to do so is crucial for Brouwer’s proof of the Bar Theorem.

In the same pages, Heyting also gave the following justification of Ex Falso:

Axiom X [\(\neg p \rightarrow(p \rightarrow q)\)] may not seem intuitively clear. As a matter of fact, it adds to the precision of the definition of implication. You remember that \(p \rightarrow q\) can be asserted if and only if we possess a construction which, joined to the construction \(p\), would prove \(q\). Now suppose that \(\vdash \neg p\), that is, we have deduced a contradiction from the supposition that \(p\) were carried out. Then, in a sense, this can be considered as a construction, which, joined to a proof of \(p\) (which cannot exist) leads to a proof of \(q\). (Heyting 1956: 102)

One easily recognizes Heyting’s effort to explain Ex Falso as much as possible along the same lines as other implications, namely, by providing a concrete construction that leads from the antecedent to the consequent. In its attempt to provide, “in a sense”, a construction, the explanation is clearly not of the same kind as Kolmogorov’s stipulation from 1932. But it does not fit into Heyting’s original interpretation of logic in terms of intentions directed at constructions and the fulfillment of such intentions either. For to fulfill an intention directed toward a particular construction we will have to exhibit that construction; we will have to exhibit a construction that transforms any proof of \(p\) into one of \(q\). But how can a construction that from the assumption \(p\) arrives at a contradiction, and therefore generally speaking not at \(q\), lead to \(q\)? It will not do to say that such a construction exists “in a sense”. A construction that is a construction “in a sense”, as Heyting helps himself to here, is no construction.

6. Objections to the Proof Interpretation

As the Proof Interpretation became known, through personal exchanges and in print, a number of objections were made to it:

  1. Its explanation of implication is not strict enough (Johansson)
  2. Its explanation of implication depends on hypothetical constructions, which are not in intuition (Freudenthal, Griss)
  3. Its explanation of implication is circular (Gentzen)
  4. Its explanation of implication is impredicative (Gödel, Kuroda, Kreisel)
These criticisms also targeted the universal quantifier and negation, which are both closely related to implication. Whether the criticisms are justified or not, they inspired important innovations:
  1. Normalization for first-order intuitionistic predicate logic (Gentzen)
  2. Minimal logic (Johansson)
  3. Functional interpretations (Gödel)
  4. Negationless mathematics (Griss)
Thematically, the objections of Johansson, Freudenthal, and Griss are closely related, as are those of Gentzen and Gödel, Kuroda, and Kreisel. In a discussion of the Proof Interpretation as a codification of Brouwer’s explanation of logic, the former three are potentially the strongest ones as they were formulated from a point of view that was either avowedly intuitionistic (Freudenthal, Griss), or close enough to be interpreted that way (Johansson). That was less the case for Gentzen, and certainly less for Gödel; on the other hand, their objections have had a much wider influence, corresponding to the fact that intuitionism has remained a minority view. For the moment, we will discuss the first group.

6.1 Implication is Not Strict Enough (Johansson 1935–1937)

As mentioned in section 4.4 above, Heyting’s axiomatization of implication was soon questioned by Johansson. Ingebrigt Johansson (1904–1987) was a Norwegian mathematician working mostly in geometry and topology. He had found a reference to Heyting’s “Die formalen Regeln” (Heyting 1930) by accident.[35] “Having studied it carefully, I have become able to understand works by Brouwer to some extent; before, that was impossible for me” (Johansson to Heyting, August 29, 1935; translation mine). His concern over the acceptability of Ex Falso (axiom \ref{HeytingAxiom10} above) led to a short correspondence from later 1935 to early 1936,[36] and resulted in the publication of “Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus” (Johansson 1937) in Brouwer’s Compositio Mathematica. Here I will only discuss Johansson’s direct criticism of the Proof Interpretation; evidently, this does not do much justice to his ideas that allowed him not only to criticize the Proof Interpretation but to turn that criticism into the positive development of Minimal Logic.

Johansson announces his disapproval of the inclusion of Ex Falso in the opening letter but first formulates a precise criticism in his second:

I have not been able to make my peace with Axiom 4.1. You say that when \(a \rightarrow b\) has been proved, and later \(\neg a\) is proved, then \(a \rightarrow b\) should remain correct. Indeed; but \(\vdash \neg a \rightarrow \cdot a \rightarrow b\) means that when \(\neg a\) has been proved, \(b\) at once becomes derivable from \(a\), even when this had not been proved before. And that contradicts my intuition in the most violent way. (Johansson to Heyting, September 23, 1935; translation mine)

And later that year:

My being unwilling to accept 4.1 is in the end simply based on the circumstance that I prefer to work with a more strict implication. My Minimal Logic shows, however, that a more strict implication really is possible. (November 15, 1935; translation mine):

(The phrase “strict implication” is a reference to Lewis 1914, which Johansson will cite in his article of 1937.)

In a note for his reply (and presumably also in the letter actually sent) Heyting explained:

I interpret \(a \rightarrow b\) as “to reduce the solution of \(b\) to that of \(a\), or to show the impossibility of solving \(a\)”. This interpretation is appropriate. (Note by Heyting to Johansson’s letter of September 23, 1935; translation mine)[37]

This of course is Kolmogorov’s interpretation of 1932 (see section 5.3 above).

In 1955, in the French translation of his book Grundlagenforschung of 1934, Heyting adds a note saying that Johansson’s interpretation of the implication is different from his own (Heyting 1955: 19). But the discussion seems to have had an effect on Heyting. The second thoughts that Heyting seems to have developed about Kolmogorov’s interpretation as applied to Ex Falso are probably related to Johansson’s insistence that \(\neg a \rightarrow \cdot a \rightarrow b\) can only be accepted if a construction can be indicated that, on the assumption that \(\neg a\) has been proved, transforms proofs of \(a\) into proofs of \(b\). For in the justification of Ex Falso that Heyting went on to give in his book of 1956, Intuitionism. An introduction, he tried to make the case that there indeed is a construction that will do just that; see the discussion in section 5.4 above.

Formalized intuitionistic logic with Ex Falso is interpretable in Minimal Logic (Prawitz & Malmnäs 1968: 219, 221, 224–225). In this translation, \(\bot\) is replaced by an arbitrary proposition letter that does not occur in the original proof. From a contentual point of view, the problem of finding an acceptable meaning for the formulas containing that proposition letter would of course remain.

However, for the specific systems of formalized primitive recursive arithmetic (PRA) and Heyting Arithmetic (HA) there is a result that is more satisfying from the contentual point of view. Defining \(\bot\) as \(0=1\) enables one formally to derive \(\bot \rightarrow A\) for any \(A\) in the language of the system. The demonstration of this fact (Troelstra & van Dalen 1988: 126–127) does not depend on knowing that there is no proof of \(0=1\), and the demonstration makes it easy to see how in these systems from a formal proof of \(0=1\) one would obtain a formal proof of any given \(A\).

For a discussion of other logical aspects of the Heyting-Johansson correspondence, see van der Molen 2016. On negation in Minimal Logic, see Hazen 1995. Relations between the logic of Kolmogorov 1925 and Minimal Logic are discussed in Plisko 1988. Proof-theoretical aspects of Minimal Logic are treated in Prawitz 1965 and Prawitz & Malmnäs 1968; model-theory in Fitting 1969: 40, Georgacarakos 1982, and Mendez 1988; an algebraic approach in Rasiowa 1974: chapter 11. Weakenings of Minimal Logic are the subject of Colacito, de Jongh, & Vargas 2017.

6.2 Hypothetical Constructions Are Not in Intuition (Freudenthal 1937, Griss 1941–1951)

To have a genuine implication (and hence also a genuine universal quantification) it must be possible to make hypotheses; that this is possible in intuitionism was contested by the intuitionists Freudenthal and Griss. They did not comment directly on the passage in Brouwer’s dissertation discussed above in section section 2.2, in which Brouwer argues that arguments that seem to involve hypothetical constructions in reality do not. Both Freudenthal and Griss must have known that argument. Conversely, although Brouwer did react in print to both (see below), this regrettably did not include an explicit philosophical engagement with their views. He did express himself at a meeting of the Dutch Mathematical Society at the Krasnapolsky Hotel in Amsterdam in 1947, as remembered by Korevaar:

That day G.F.C. Griss (mathematics teacher in Gouda) spoke about what he called his negationless mathematics. That was even more strict than Brouwer’s intuitionism. […] Afterwards there was an extended discussion at the blackboard. First between Griss and, among others, van Dantzig, who evoked his affirmative mathematics. I think that Freudenthal was there, too. Then it was Heyting’s turn; he tried to explain what Brouwer had meant. Finally, and unexpectedly, Brouwer himself appeared, from the back of the room; no one had noticed that he had arrived. Brouwer came forward running, his coat-tails flapping. And he cried: “You have all misunderstood!” (Korevaar 2016: 248; translation mine)

Unfortunately, no report seems to exist on the content of the discussion.

Two years later the Belgian philosopher S.I. Dockx hoped to organize a meeting on negationless logic with Brouwer, Griss, Freudenthal, Heyting, and van Dantzig. Brouwer made it clear, however, that he did not want to participate in an event together with Freudenthal (letter of Beth to Dockx of July 8, 1949, in van Dalen 2011: Online Supplement, 2446; for Brouwer’s conflict with Freudenthal see van Dalen 2005: 721–728, 753–757, and 794–799). In the end, a colloquium was indeed held in Brussels in 1949, with as speakers Beth, Destouches-Février, Feys, Freudenthal, Griss and van Dantzig (Chronique générale 1949: 435).[38] As is the case for the meeting in Amsterdam in 1947, there seems to exist no report on the content of the discussions; and Heyting’s absence from the list of speakers is as yet unaccounted for.

6.2.1 Freudenthal 1937

Hans Freudenthal (1905–1990) was an intellectually omnivorous German-Dutch mathematician, who took his PhD in Berlin in 1930 with a thesis in topology directed by Brouwer’s friends Hopf and Bieberbach. He came to know Brouwer when the latter lectured in Berlin in 1927, and made a favorable impression on him because of the good questions he asked (van Dalen 2005: 546). In 1930 he moved to Amsterdam to become one of Brouwer’s assistants and, from 1931, also lecturer. At the same time he continued his research in avant-garde topology. After the Second World War, Freudenthal became full professor in Utrecht, and mostly did important work in the history and didactics of mathematics. (In the preface to Mathematics as an Educational Task he wrote “My educational interpretation of mathematics betrays the influence of L.E.J. Brouwer’s view on mathematics (though not on education)”, Freudenthal 1973, ix.) He also edited the second volume of Brouwer’s Collected Works, which contains in particular the papers on topology (Brouwer 1977).

In 1937 Freudenthal formulated two objections to explanations of implication such as Heyting’s and Kolmogorov’s. One is that a hypothetical construction of the antecedent provides no actual construction material at all, so that, if the idea of a construction that proves \(a \supset b\) is to make intuitionistic sense, this could only be done by giving a proof of \(b\) via a proof of \(a\). The second objection is that, moreover, the antecedent \(a\) cannot even be given a definite meaning without thereby proving it; so that

in the Heyting-Kolmogorov explanation the value of implication becomes illusory, as the hypothesis, in its quality as hypothesis, immediately eliminates itself. (Freudenthal 1937b: 115)

Freudenthal arrives at this point because of his view that, more generally, a proof is precisely what gives a statement its definite meaning:

It lies close to hand to explain a statement as the establishing of a fact, of the obtaining of which one has convinced oneself by a proof, i.e., by bringing about the relation expressed in the statement. But this explanation can only be given cautiously, because once a statement is the establishing of a fact, there is no justification anymore of the separation of statement and proof. When I say, for example, that the sequence \(a_{\nu}\) converges positively to \(a\), this is only an abbreviated way of stating the fact that for every \(n\) an \(N\) can be determined such that \(a-a_{\nu}\) ≤ 1/\(n\) for \(\nu\) ≥ \(N\). That for every \(n\) an \(N\) with this property can be determined, is a statement that has intuitionistic sense only if one has a computation method that generates the \(N\) from each \(n\), a computation method that can roughly be represented by a formula into which \(a_{\nu}\) and \(a\) enter in some way. This example shows that each statement, once one formulates it in an intuitionistically unobjectionable way, automatically contains its full proof. (Freudenthal 1937b: 112; translation mine)

Behind the example Freudenthal gives here is the general intuitionistic idea that mathematical facts can only consist in the existence of constructions and proofs (which are themselves special constructions), so that spelling out a mathematical fact amounts to specifying the constructions that bring it about; but that is also, Freudenthal points out, what a proof is. Absent a proof, a statement has at most a heuristic or provisional meaning.

Negative statements are no exception according to Freudenthal, because their meaning is that all attempts at a construction with certain properties fail to achieve their aim, and a survey of these failings (which may depend on complete induction) constitutes the proof of the negative statement. Note that, as a consequence, meaning would not be compositional: The unnegated statement has no non-heuristic meaning of its own. This notion of heuristic meaning, which is the only kind of meaning an unnegated statement can have until the survey of attempts at constructions for it has been completed, must still be sufficiently precise if it is to serve as the basis of a mathematical proof of a negated statement. This goes in the direction of reading \(\beta\) of implications in section 2.2 above; perhaps the difference with Brouwer is not so great on this point.

Freudenthal accepts a special but important case of implication, the kind that is implicit in general statements such as “A total function on [0,1] is uniformly continuous”. In general statements

the subject is the function, finitary set, number (as element of a set), understood in their wholly free growth. Neither specific nor all specific elements of a whole are meant, but the function, the finitary set, the element of a set, an individual therefore, albeit a peculiar individual, a true Proteus, very peculiar in this respect, that it may arrive that one is considering two different exemplars of this individual. (Freudenthal 1937b: 115; translation mine)

The assertion then is understood as of a relation between two predications of one specific subject, The example is then understood as the subject being the function and the predicates “being restricted in its free growth to being total on [0,1]” and “being restricted in its free growth to being uniformly continuous” (Freudenthal 1937b: 115).

Freudenthal acknowledges the alternative of reading it as asserting the containment of the species of total functions in the species of uniformly continuous ones, but finds a reading in terms of a freely growing object “intuitionistically more sympathetic” (Freudenthal 1937b: 116). He comments without further explanation that this is “so to speak a cataloguing of the species” (Freudenthal 1937b: 116). This remark in fact draws on his other publication in that issue of Compositio Mathematica, on intuitionistic topology. There he gives a definition of which the relevant part is this: [39]

A sequence of things \(A_n (n=1,2,\ldots)\) is called catalogued, if to every \(A_n\) is assigned the expression \(\ne 0\) and to each \(A_{\mu_1}A_{\mu_2} \ldots A_{\mu_k}\) the expression \(= 0\) or \(\ne 0\) (but never both expressions) (Freudenthal 1937a: 84; translation mine)

In a footnote, it is added that the sequence of things \(A_n\) need not be lawlike, but may be growing in more or less freedom. Among the conditions on these assignments is specified that of extensibility:

If \(A_{\mu_1}A_{\mu_2}\ldots A_{\mu_{ k} } \ne 0\), an \(m \ne \mu_1, \mu_2,\ldots,\mu_k\) can be indicated such that \(A_{\mu_1}A_{\mu_2}\ldots A_{\mu_{ k} }A_{\mu_m} \ne 0\) (Freudenthal 1937a: 84; translation mine)

In these terms, the content of the example theorem, “A total function on [0,1] is uniformly continuous”, may be stated as follows. To a species one assigns the expression \(\ne 0\) if a freely growing object can be restricted so as to have the corresponding property; and to a sequence of species the expression \(\ne 0\) if a freely growing object can be restricted to have all the corresponding properties, and 0 if it cannot. Then a sequence of species \(\ne 0\) containing the species of functions that are total on [0,1] may always be extended with the species of functions that are uniformly continuous.

That Freudenthal finds this reading “intuitionistically more sympathetic” is probably because it is more transparently related to the intuitionistic idea that, on the hand, when we set out to construct an object we set out to construct an object of a certain type, and on the other hand that object will acquire properties in acts of construction over time. Freudenthal’s Protean individuals are rather suggestive of the later idea, from computer science, of generic prototype objects in certain programming languages (on the latter see e.g., Blaschek 1994). These can indeed be treated as individuals that have multiple instantiations, and properties can be added to them over time.

Freudenthal acknowledges that it remains to be seen whether his proposal can be carried out. De Iongh (1949) comments that Freudenthal in effect accepts Russell’s notion of formal implication (Russell 1903: section 12) as a primitive (Freudenthal does not mention Russell). In fact, Russell does not merely find the understanding of general implication as a containment relation less sympathetic, but mistaken (Russell 1903: section 77). On the other hand, Russell’s formal implication is construed as a relation between two propositional functions, and owes its generality to the fact that these take as arguments any value in the domain, whereas Freudenthal’s implication is a relation between two predications of an individual, and owes its generality to the fact that the individual in question is not any specific function but “the function in its free growth”.

As on this construal a proof of a general statement is in fact a proof for one peculiar individual, each instantiation of the general statement for another, normal individual needs its own proof (which will proceed along the exact same lines). Freudenthal accepts this:

The general proof, given once, serves us no more than a map, which indeed facilitates the ascent of a mountain for us, but does not spare it. (Freudenthal 1937b: 116; translation mine)

This is also the case when an appeal is made to lemmas that are stated schematically, such as \(m+n = n+m\). Freudenthal readily acknowledges that in linguistic representations of proof one will not do this, but considers this a way in which a linguistic representation fails to capture what a proof is.

Freudenthal’s paper was followed by comments from Heyting.[40] Heyting agrees with Freudenthal’s thesis that if a mathematical statement is explained as the linguistic expression of a fact, then the meaning of the statement is given by its proof.[41]

But at the same time he holds that posing a mathematical problem is not the same as making a mathematical assertion, and that this difference allows for an understanding of implications whose antecedent has not been established. An example he gives is that it is obviously correct to say that if \(\pi\) contains the sequence 0123456789, then it contains the sequence 012345678 (Heyting 1937: 117). (At the time there was no proof of the antecedent. In 1997 a computer program calculated that at the 17,387,594,880th digit after the decimal point in \(\pi\), a sequence 0123456789 begins (Borwein 1998). One easily modifies Heyting’s example appropriately.) This is so, because we know how to turn solutions of the problem of finding a sequence 0123456789 into solutions of the problem of finding a sequence 012345678.

Furthermore, Heyting doubts that Freudenthal’s notion of an individual of which there may exist different exemplars clarifies matters. In his view, one would have to represent the collection of proper individuals by elements of a spread, so as to be able to explain universal quantification over these individuals in terms of the continuity principle for choice sequences applied to the sequences in the representing spread. But he observes that in that case Brouwer’s theorem that all total functions on the unit continuum are continuous cannot be reconstructed: The continuity of these functions is in fact a condition of the possibility of their representation in a spread. Brouwer published the proof of this representation theorem in his 1942B, to which the reader is referred for further details. That publication was clearly occasioned by a renewed interest on Brouwer’s part in the Freudenthal-Heyting exchange (see the opening lines of Brouwer 1942A).

Freudenthal (1937c) replied to Heyting in turn, but most briefly. He denies that with a reading in terms of problems and solutions the proper intuitionistic meaning, that is, one that does not depend on language and is not heuristic, has been found; and he considers it improbable that intuitionistic predicate calculus applies only to spreads, not to species.

The referee for the journal Compositio Mathematica, in which this exchange between Freudenthal and Heyting appeared, was Brouwer. His report read:

Interesting discussion on the sense of one sentence being implied by another, when nothing is known about the correctness of the latter sentence. (As quoted and translated in Sundholm & van Atten 2008: 70)

One would have hoped to see Brouwer’s actual thoughts on the matter. On the other hand, as pointed out by van Dalen and Remmert (2007: 183), Brouwer was here playing both the role of referee and of editor in chief, so the only person meant actually to read this report was he.

To the extent that Freudenthal’s rejection of implication implies a rejection of negation defined as \(A \rightarrow \bot\), whatever momentum Freudenthal’s objection may have had was taken over a few years later by the work of Griss; it seems that Griss was not aware of Freudenthal’s paper of 1937. Freudenthal’s proposed explanation of universal quantification seems not to have been developed any further within the tradition.

6.2.2 Griss 1941–1951

Starting in 1941, Georg François Cornelis Griss argued that negation, and hence a whole class of implications, should be banished from intuitionism. Griss (1898–1953) had received his PhD in Amsterdam in 1925 for a thesis in differential geometry supervised by Weitzenböck, but had attended courses by Brouwer and was very sympathetic to intuitionism. (Most biographical details in this section come from van Rootselaar 1953–1954 and Pos 1953–1954.)

In a letter to Brouwer of April 19, 1941, he stated the point of departure for his negationless mathematics as follows:

Showing that something is not true, i.e., showing the incorrectness of a hypothesis, is not an intuitively clear act. Of a hypothesis, which later turns out to be even wrong, one cannot possibly have an intuitively clear representation. One must maintain the demand that only building things up from the foundations makes sense in intuitionistic mathematics. (van Dalen 2011: Online Supplement, 2142; translation mine)

Insisting on intuitively clear representations throughout, Griss also holds that “to define is to construct” (Griss 1947: 69): a definition is meaningful only if it specifies a construction of the object defined.

Thus the notion of negation, understood as implication of a falsehood, is rejected. In Idealistische Filosofie (1947: 24), Griss repeats the above passage and points out this is in accord with criticism of negation by Bergson in L’Évolution créatrice (Bergson, 298–322); a rare occasion on which a Brouwerian intuitionist refers to the French philosopher of intuition. (Brouwer never discussed Bergson; see van Stigt 1990: 152–153 and 324 for differences between their conceptions, and also Hesseling 2003: sections 6.3.1–6.3.6.)

The fundamental point of agreement Griss finds with Bergson is that the only meaningful construal of negation consists in the positive notion of distinguishability. For example, the distinguishability of 1 and 2 is not defined as pure negation of their identity, but is an intuitive given based on their generation from the basic intuition of two-ity. For other objects, such as rational numbers and real numbers, the notion of distinguishability may be defined in terms of that of the natural numbers. With the rejection of negation also came a rejection of empty species, so that the intersection of two species exists only if they have an element in common. Griss is surprised to report that he has encountered more opposition against the rejection of empty species than against the avoidance of negation. (Griss 1951a: 45)

Griss acknowledges a role for problems and solutions in research (in terms of which Kolmogorov and Heyting understood logic, including negation); but he does not consider these to belong to mathematics proper:

To negationless intuitionistic mathematics belong only constructions and properties in relation to those constructions. Posing problems and asking for solutions are premathematical activities. It goes without saying that in those premathematical investigations negation may be used just as well as all kinds of other means, like the principle of the excluded middle or even a physical experiment. (Griss 1948a: 72; translation mine)

Presumably, then, this would have determined his reply if Heyting had leveled the same objection to Griss’ position as he had done to Freudenthal’s, the objection that it is obviously correct to say that if \(\pi\) contains the sequence 0123456789, then it contains the sequence 012345678.

Indeed, it is clear that Griss’ conception has much in common with that of Freudenthal. At the same time, Griss’ notion of the “premathematical” seems to be much wider than Freudenthal’s of the “heuristic”. After all, for Freudenthal it was possible mathematically to prove a negative statement by showing that all ways to make the unnegated statement true by supplying an appropriate construction must fail. For Griss this is clearly excluded. (It seems Freudenthal and Griss never commented in print on each other’s positions. Note also that Griss, in his long letter to Brouwer of 1941 mentioned above that launched his program, does not refer to Freudenthal.)

Since negationless mathematics accepts only true propositions, its propositional logic contains only conjunction &, with implication as a special case: “The implication \(p \rightarrow q\) will have its natural meaning: \(q\) follows from \(p\), \(p\) is true, so \(q\) is also true” (Griss 1951a: 41). However, an interpretation of Heyting’s propositional logic in this logic of & and \(\rightarrow\) becomes possible by construing it as a logic of classes or species (Griss 1948b, 1951a). A basic species, for example that of the natural numbers, is taken as given, and all others will be constructed as subspecies of it. Then \(\neg a\) can be defined as the complement of a relative to the basic species and \(a \vee b\) is the union of \(a\) and \(b\). Thus, Griss (1951a) applied the strategy Heyting had used in 1928 to Heyting’s own formalization and deleted the parts that are not acceptable in negationless mathematics (while adding axioms and conditions to ensure that species be inhabited).

Axioms for an interpretation of predicate logic are obtained from those for propositional logic (Griss 1951a: 48). One substitutes \(a(x)\) for \(p\) everywhere, and prefixes all axioms in which \(x\) occurs with \(\forall x\). The meaning of \(a(x)\) is that \(x\) is an element of the species \(a\), and \(\forall x(a(x) \rightarrow b(x))\), is defined as \(a \subset b\). (See below for a further remark on this in relation to a criticism voiced by Heyting in 1955.)

Treating intuitionistic mathematics according to Griss’ principles requires a substantial reconstruction. After a first mathematical sketch of his project in Dutch (Griss 1944), Griss made an informal start with parts of intuitionistic arithmetic, the theory of real numbers, and projective geometry in a series of papers published between 1946 and 1951 (Griss 1946, 1950, 1951b,c,d).

Griss was not able to continue that series, as in 1951 an illness began that would lead to his early death in 1953. However, he was able to act as the unofficial adviser of Nicolle Dequoy, who defended a doctoral thesis on negationless projective geometry at the Université de Paris in 1952 (published as Dequoy 1955). Formal work on negationless logic in Griss’ sense was done by Destouches-Février (1948),[42] Gilmore 1953a, 1953b, and 1953c, Vredenduin 1953, Valpola 1955, Nelson 1966. This line of work culminated in Krivtsov 2000a, 2000b, 2000c, which give a comprehensive modern treatment of negationless predicate logic, arithmetic, analysis, and higher-order arithmetic.

When Griss began to elaborate the negationless intuitionistic mathematics that he proposed, Brouwer and Heyting supported his career in two ways. From 1944 to 1951, they communicated Griss’ papers to the Royal Dutch Academy of Sciences;[43] and in 1949 they used their influence to reduce Griss’ teaching load at the high school in Gouda where he worked (van Rootselaar 1953–1954: 43).

But while supporting the publication of Griss’ papers, Brouwer at the same time presented a counterargument to one of Griss’ examples that implied that he did not support Griss’ philosophical claim.[44] In his letter to Brouwer of 1941, Griss had remarked that

No real number is known about which it has been proved that it cannot possibly be equal to 0 \((a \ne 0)\) while at the same time it has not been proven that the number differs positively from 0 (\(a \mathbin{\#} 0\)). (van Dalen 2011: 405)

(\(a \mathbin{\#} b\), the apartness relation, is defined as \(\exists n(|a-b| \gt (1/2)^n)\).) Brouwer went on to publish a construction of a real number with just that property in “Essentially negative properties” (1948A). Brouwer’s argument, while suggestive, is perhaps not wholly conclusive: although it does show that the most obvious candidate for a positive equivalent fails, it does not show that there can be no such equivalent (Krivtsov 2000a: 167). Moreover, Brouwer did not make explicit how his own philosophical understanding of negation differed from that of Griss.

In 1949, David van Dantzig argued that the method that Brouwer had used in devising his example of an essentially negative property, which has become known as the method of the creating subject (section 3.3), depended on the untenable thesis “that there will ‘always’ be a human being willing and capable” of working on open problems (van Dantzig 1949: 951). Brouwer replied, in personal correspondence, that any psychological interpretation of intuitionism is incorrect (van Dalen 2011: 439; van Atten 2004b: chapter 6 for discussion). Note that, whether correct or not, this objection does not hinge on the possibility of negation as such.

Van Dantzig also pointed out that Brouwer’s construction cannot be used as an argument against Griss’ position, on pain of circularity:

In any case it seems impossible to define Brouwer’s use of the term “absurd” without using another negative term (like “contradiction”), in other words it seems to be unavoidable to consider Brouwer’s general form of the negation as an “entité primitive”, irreducible to affirmative concepts. Therefore Brouwer’s theorem can not invalidate the attempts of other mathematicians (in particular G.F.C. Griss, Mrs. P. Destouches-Février and the present author) to do without the concept of negation. On the contrary, it shows again, how unclear the concept of “absurdity” is, and makes its avoidance appear more desirable. (van Dantzig 1949: 952)

On the other hand, while it is clear that Brouwer himself did not share these objections to absurdity, he had opened his article not by saying that he wrote it to refute but “to estimate the significance of affirmative or negationless mathematics, the development of which is sometimes advocated” (Brouwer 1948A: 963).

The “affirmative mathematics” mentioned in these quotations from van Dantzig and Brouwer was proposed by van Dantzig as a formal system for classical mathematicians to reason about numerical calculations and empirical problems (van Dantzig 1947b, 1951). It contains neither negation nor disjunction, although in certain contexts weak versions of these can be defined, and existential quantifiers must be bounded.[45] Presented as “intuitionistic mathematics from a formal standpoint”, it does not aim to be a philosophical foundation of a logic for intuitionistic mathematics.[46]

In 1955, Heyting objected to Griss’ position that it made it impossible to express generality:

If we say, “For all real numbers \(a\) and \(b\), \(a+b = b+a\)”, this means the same as “If we construct two real numbers \(a\) and \(b\), then \(a+b = b+a\)”, but we have not actually constructed them. (Heyting 1953–1955: 95)

Taking this line further, a proof of the general statement would require the actual construction of all pairs of real numbers (and then showing that for each pair the equality holds), which is impossible. But in a review of Heyting’s paper, Vredenduin replied that the Grissian meaning is this:

As soon as you have realized two real numbers \(a\) and \(b\), you can be certain that \(a + b = b + a\). This would be meaningless only if real numbers were unrealizable. (Vredenduin 1956: 91)

Accordingly, what a general statement expresses directly is not a property of actual constructions, nor of unactual ones, but the correctness of a rule that applies to actual constructions. The premisse of the rule then means no more than “Let \(a\) and \(b\) be any two real numbers that we have constructed”. Griss would accept that as meaningful because he supplied a notion of real number and a construction method that shows that the species of real numbers thus construed is inhabited. Compare:

The well-known turn in mathematics: “Suppose ABC to be rectangular” seems to be a supposition, but mostly means: “Consider a rectangular triangle ABC”. (Griss 1950: 456)

For further philosophical discussion of affirmative and negationless mathematics, see Apostel 1972; Beth 1966: 436–439; Fraenkel et al. 1973: 249–251; Franchella 1994b; Franchella 2008: 57–68; Heyting 1953–55; Heyting 1956: section 8.2. For an algebraic study of negationless logic see Imai & Iseki 1966 and Arruda1978; the latter also compares Griss’ and Vredenduin’s systems with one another. Modern formalizations of negationless systems are given in Krivtsov 2000a,b,c.

Griss’ negationless logic has been connected to the Curry-Howard isomorphism (e.g., Colson & Michel 2007, 2008, 2009; Michel 2008) and to the Calculus of Constructions (Demange 2012). These authors speak of “pedagogical logic”, as it reflects the pedagogical ideal that newly introduced hypotheses and definitions be motivated by examples.

An example of recent mathematical work that finds inspiration in the negationless approach is Veldman 2008.

Finally, this entry has not, as yet, discussed precursors to Brouwer, more intricate aspects of Brouwer’s “strong counterexamples”, the objections to the Proof Interpretation of circularity and impredicativity, or the later developments around the Proof Interpretation. These will be subject of future updates.

Bibliography

Brouwer’s writings are referred to according to the scheme in the bibliography van Dalen 1997a; Gödel’s, according to the bibliography in Gödel 1986, Gödel 1990, Gödel 1995 (except for Gödel 1970); Heyting’s, according to the bibliography Troelstra et al. 1981 (except for Heyting 1928).

  • Apostel, L., 1972, “Negation: The tension between ontological positivity (negationless positivity) and anthropological negativity (positively described)”, Logique et Analyse, 15(57–58): 209–317. [Apostel 1972 available online]
  • Artemov, Sergei N., 2001, “Explicit provability and constructive semantics”, Bulletin of Symbolic Logic, 7(1): 1–36. doi:10.2307/2687821
  • Arruda, Ayda Ignez, 1978, “Some remarks on Griss’ logic of negationless intuitionistic mathematics”, in Mathematical Logic, Proceedings of the 1st Brazilian Conference on Mathematical Logic, Campinas 1977 (Lecture Notes in Pure and Applied Mathematics 39), A.I. Arruda, N.C.A. da Costa, R. Chuaqui (eds.), 9–29.
  • van Atten, Mark, 2004a, “Review of Dennis E. Hesseling, Gnomes in the Fog. The Reception of Brouwer’s Intuitionism in the 1920s”, Bulletin of Symbolic Logic, 10(3): 423–427. doi:10.2307/3185194
  • –––, 2004b, On Brouwer, Belmont, CA: Wadsworth.
  • –––, 2005, “The correspondence between Oskar Becker and Arend Heyting”, in Oskar Becker und die Philosophie der Mathematik, V. Peckhaus (ed.), München: Wilhelm Fink, 119–142.
  • –––, 2009, “The hypothetical judgement in the history of intuitionistic logic”, in Logic, Methodology, and Philosophy of Science 13: Proceedings of the 2007 International Congress in Beijing, C. Glymour, W. Wang, and D. Westerståhl, eds., London: King’s College Publications, 122–136.
  • van Atten, Mark, Göran Sundholm, Michel Bourdeau, and Vanessa van Atten, 2014, “‘Que les principes de la logique ne sont pas fiables.’ Nouvelle traduction française annotée et commentée de l’article de 1908 de L.E.J. Brouwer”, Revue d’Histoire des Sciences, 67(2): 257–281. doi:10.3917/rhs.672.0257
  • van Atten, Mark, Pascal Boldini, Michel Bourdeau, and Gerhard Heinzmann (eds.), 2008, One Hundred Years of Intuitionism (1907–2007). The Cerisy Conference, Basel: Birkhäuser. doi:10.1007/978-3-7643-8653-5
  • van Atten, Mark and Göran Sundholm, 2017, “L.E.J. Brouwer’s ‘Unreliability of the logical principles’: A new translation, with an introduction”, History and Philosophy of Logic, 38(1): 24–47. doi:10.1080/01445340.2016.1210986
  • Barzin, M. and A. Errera, 1927, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 13: 56–71.
  • Bazhanov, Valentin A., 2003, “The Scholar and the ‘Wolfhound Era’: The Fate of Ivan E. Orlov’s Ideas in Logic, Philosophy, and Science”, Science in Context, 16(4): 535–550. doi:10.1017/S0269889703000954
  • Becker, Oskar, 1927, “Mathematische Existenz. Untersuchungen zur Logik und Ontologie mathematischer Phänomene”, Jahrbuch für Philosophie und phänomenologische Forschung, 8: 439–809.
  • –––, 1930, “Zur Logik der Modalitäten”, Jahrbuch für Philosophie und phänomenologische Forschung, 11: 497–548.
  • Benacerraf, Paul and Hilary Putnam (eds.), 1983, Philosophy of Mathematics: Selected Readings, second edition, Cambridge: Cambridge University Press. doi:10.1017/CBO9781139171519
  • Bergson, Henri, 1907, L’Évolution Créatrice, Paris: Félix Alcan.
  • Bernays, Paul, 1926, “Axiomatische Untersuchung des Aussagen-Kalküls der ‘Principia Mathematica’”, Mathematische Zeitschrift, 25: 305–320. doi:10.1007/BF01283841
  • –––, 1967, “Hilbert, David”, in The Encyclopedia of Philosophy, vol. 3, Paul Edwards (ed.), New York: Macmillan.
  • Beth, Evert W., 1956, “Semantic Construction of Intuitionistic Logic”, Mededelingen der Koninklijke Nederlandse Akademie van Wetenschappen. Afdeling Letterkunde, 19(11): 357–388.
  • –––, 1966, The Foundations of Mathematics: A Study in the Philosophy of Science, second revised edition, New York: Harper & Row.
  • Blaschek, Günther, 1994, Object-Oriented Programming: with Prototypes, Berlin: Springer. doi:10.1007/978-3-642-78077-6
  • Borwein, Jonathan M., 1998, “Brouwer-Heyting Sequences Converge”, Mathematical Intelligencer, 20(1): 14–15. doi:10.1007/BF03024393
  • Brouwer, L.E.J., 1907, Over de Grondslagen der Wiskunde (On the Foundations of Mathematics), Ph.D. thesis, Universiteit van Amsterdam. English translation in Brouwer 1975: 11–101.
  • –––, 1908C, “De onbetrouwbaarheid der logische principes” (The Unreliability of the Logical Principles), Tijdschrift voor Wijsbegeerte, 2: 152–158. English translation in Van Atten and Sundholm 2017. An older English translation is in Brouwer 1975: 107–111. doi:10.1016/B978-0-7204-2076-0.50009-X
  • –––, 1918B, “Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre”, KNAW Verhandelingen, 5: 1–43. Also in Brouwer 1975: 150–190 (in German). doi:10.1016/B978-0-7204-2076-0.50015-5
  • –––, 1919A, “Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Zweiter Teil, Theorie der Punktmengen”, KNAW Verhandelingen, 7: 1–33. Also in Brouwer 1975: 191–221 (in German). doi:10.1016/B978-0-7204-2076-0.50016-7
  • –––, 1919D, “Intuitionistische Mengenlehre”, Jahresbericht D.M.V., 28: 203–208. English translation in Mancosu 1998: 23–27.
  • –––, 1921A, “Besitzt jede reelle Zahl eine Dezimalbruchentwicklung?”, Mathematische Annalen, 83(3–4): 201–210. English translation in Mancosu 1998: 28–35. doi:10.1007/BF01458382
  • –––, 1924D1, “Bewijs dat iedere volle functie gelijkmatig continu is”, KNAW verslagen, 33: 189–193. English translation in Mancosu 1998: 36–39.
  • –––, 1924N, “Über die Bedeutung des Satzes vom ausgeschlossenen Dritten in der Mathematik, insbesondere in der Funktionentheorie”, Journal für die reine und angewandte Mathematik, 154: 1–7. English translation in van Heijenoort 1967: 335–341.
  • –––, 1925E, “Intuitionistische Zerlegung mathematischer Grundbegriffe”, Jahresbericht D.M.V., 33: 251–256. English translation in Mancosu 1998: 287–289 (sections 2–4), 290–292 (section 1).
  • –––, 1926A, “Zur Begründung der intuitionistischen Mathematik, II”, Mathematische Annalen, 95: 453–472. doi:10.1007/BF01206621
  • –––, 1926B2, “Intuitionistische Einführung des Dimensionsbegriffes”, Proceedings Koninklijke Akademie van Wetenschappen Amsterdam, 29: 855–873.
  • –––, 1927B, “Über Definitionsbereiche von Funktionen”, Mathematische Annalen, 97: 60–75. English translation of sections 1–3 in van Heijenoort 1967: 457–463. doi:10.1007/BF01447860
  • –––, 1928A2, “Intuitionistische Betrachtungen über den Formalismus”, Proceedings Koninklijke Akademie van Wetenschappen Amsterdam, 31: 374–379. English translation in Mancosu 1998: 40–44. [Brouwer 1928A2 available online]
  • –––, 1929A, “Mathematik, Wissenschaft und Sprache”, Monatshefte für Mathematik und Physik, 36: 153–164. English translation in Mancosu 1998: 45–53. doi:10.1007/BF02307611
  • –––, 1930A, Die Struktur des Kontinuums, Wien: Komitee zur Veranstaltung von Gastvorträgen ausländischer Gelehrter der exakten Wissenschaften. English translation in Mancosu 1998: 54–63.
  • –––, 1933A2, “Willen, weten, spreken” (Volition, Knowledge, Language), in De Uitdrukkingswijze der Wetenschap, L.E.J. Brouwer et al., Groningen: Noordhoff, 45–63. English translation in van Stigt 1990: 418–431. Partial English translation in Brouwer 1975: 443–446.
  • –––, 1942A, “Zum freien Werden von Mengen und Funktionen”, Proceedings Nederlandse Akademie van Wetenschappen Amsterdam, 45: 322–323. Also Indagationes Mathematicae, 4 (1942): 107–108.
  • –––, 1942B, “Die repräsentierende Menge der stetigen Funktionen des Einheitskontinuums”, Proceedings Nederlandse Akademie van Wetenschappen Amsterdam, 45: 443. Also Indagationes Mathematicae, 4 (1942): 154.
  • –––, 1948A, “Essentieel negatieve eigenschappen” (Essentially Negative Properties), Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 51: 963–964. Also Indagationes Mathematicae, 10 (1948): 322–323. English translation in Brouwer 1975: 478–479. doi:10.1016/B978-0-7204-2076-0.50053-2
  • –––, 1949A, “De non-aequivalentie van de constructieve en de negatieve orderelatie in het continuum” (The Non-Equivalence of the Constructive and the Negative Order Relation on the Continuum), Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 52:122–124. Also Indagationes Mathematicae, 11 (1949): 37–39. English translation in Brouwer 1975: 495–496. doi:10.1016/B978-0-7204-2076-0.50055-6
  • –––, 1949B, “Contradictoriteit der elementaire meetkunde” (Contradictority of Elementary Geometry), Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 52: 315–316. Also Indagationes Mathematicae, 11 (1949): 89–90. English translation in Brouwer 1975: 497–498. doi:10.1016/B978-0-7204-2076-0.50056-8
  • –––, 1949C, “Consciousness, Philosophy and Mathematics”, Proceedings of the 10th International Congress of Philosophy, Amsterdam 1948, Amsterdam: North-Holland, 3: 1235–1249.
  • –––, 1952B, “Historical Background, Principles and Methods of Intuitionism”, South African Journal of Science, 49: 139–146.
  • –––, 1954A, “Points and Spaces”, Canadian Journal of Mathematics, 6: 1–17. doi:10.4153/CJM-1954-001-9
  • –––, 1954F, “An Example of Contradictority in Classical Theory of Functions”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 57: 204–205. Also Indagationes Mathematicae, 16 (1954): 204–205. doi:10.1016/S1385-7258(54)50030-2
  • –––, 1955, “The Effect of Intuitionism on Classical Algebra of Logic”, Proceedings of the Royal Irish Academy, 57: 113–116.
  • –––, 1975, Collected Works. I: Philosophy and Foundations of Mathematics, Arend Heyting (ed.), Amsterdam: North-Holland.
  • –––, 1977, Collected Works. II: Geometry, Analysis, Topology and Mechanics, H. Freudenthal (ed.), Amsterdam: North-Holland.
  • –––, 1981A, Brouwer’s Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
  • Brouwer, L.E.J., Fred. van Eeden, J. van Ginneken, and S.J.G. Mannoury, 1937, “Signifiese dialogen”, Synthese, 2: 168–174, 261–268, 316–324. doi:10.1007/BF00880415 doi:10.1007/BF00880431 doi:10.1007/BF00880440
  • –––, 1939, Signifische dialogen, Utrecht: Erven J. Bijleveld. Partial English translation in Brouwer 1975: pp. 447–452.
  • Chronique générale, 1949. “Chronique générale”, Revue Philosophique de Louvain, 47(15): 432–436. [Chronique générale 1949 available online]
  • Colacito, Almudena, Dick de Jongh, and Ana Lucia Vargas, 2017, “Subminimal Negation”, Soft Computing, 2(1): 165–174. doi:10.1007/s00500-016-2391-8
  • Colson, Loïc, and David Michel, 2007, “Pedagogical Natural Deduction Systems: the Propositional Case”, Journal of Universal Computer Science, 13(10): 1396–1410. [Colson & Michel 2007 available online]
  • –––, 2008, “Pedagogical Second-order Propositional Calculi”, Journal of Logic and Computation, 18(4): 669–695. doi:10.1093/logcom/exn001
  • –––, 2009, “Pedagogical Second-order \(\lambda\)-calculus”, Theoretical Computer Science, 410(42): 4190–4203. doi:10.1016/j.tcs.2009.04.020
  • van Dalen, Dirk, 1973, “Lectures on intuitionism”, in Mathias & Rodgers 1973: 1–94. doi:10.1007/BFb0066771
  • –––, 1997, “A Bibliography of L.E.J. Brouwer”, Utrecht Logic Group Preprint Series, no. 175 [van Dalen 1997 updated preprint available from Universiteit Utrecht]. Updated version in van Atten et al. 2008: 343–390. doi:10.1007/978-3-7643-8653-5_22
  • –––, 1999, Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 1: The Dawning Revolution, Oxford: Clarendon Press.
  • –––, 2001a, L.E.J. Brouwer 1881–1966. Een Biografie. Het Heldere Licht van de Wiskunde, Amsterdam: Bert Bakker.
  • –––, 2001b, L.E.J. Brouwer en de Grondslagen van de Wiskunde, Utrecht: Epsilon.
  • –––, 2004, “Kolmogorov and Brouwer on constructive implication and the Ex Falso rule”, Russian Mathematical Surveys, 59(2): 247–257. doi:10.1070/RM2004v059n02ABEH000717
  • –––, 2005, Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 2: Hope and Disillusion, Oxford: Clarendon Press.
  • –––, 2008, “Another look at Brouwer’s dissertation”, in van Atten et al. 2008: 3–20. doi:10.1007/978-3-7643-8653-5_1
  • ––– (ed.), 2011, The Selected Correspondence of L.E.J. Brouwer, London: Springer. An online supplement (link and password on the copyright page of the book) presents most of the extant correspondence, but without English translations. doi:10.1007/978-0-85729-537-8
  • van Dalen, Dirk and Volker R. Remmert, 2007, “Ce périodique foncièrement international: the birth and youth of Compositio Mathematica”, Nieuw Archief voor Wiskunde 5th series, 8(3): 178–189. [van Dalen & Remmert 2007 available online]
  • van Dantzig, D., 1947a, “On the principles of intuitionistic and affirmative mathematics. I”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 50: 918–929. Also Indagationes Mathematicae, 9: 429–440.
  • –––, 1947b, “On the principles of intuitionistic and affirmative mathematics. II”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 50:1092–1103. Also Indagationes Mathematicae, 9: 506–517.
  • –––, 1949, “Comments on Brouwer’s Theorem on Essentially-negative predicates”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 52: 949–957. Also Indagationes Mathematicae, 11: 347–355.
  • –––, 1951, “Mathématique stable et mathématique affirmative”, Congrès International de Philosophie des Sciences, 1949, II Logique (Actualités scientifiques et industrielles 1134), Paris: Hermann & Cie, pp. 123–135.
  • Demange, Vincent, 2012, Vers un calcul des constructions pédagogique, PhD thesis, Université de Lorraine. Demange 2012 available from Université de Lorraine].
  • Dequoy, Nicolle, 1952 [1955], Axiomatique intuitionniste sans négation de la géométrie projective, PhD thesis, Université de Paris. Published in 1955, Paris:Gauthier-Villars (Collection de logique mathématique ; sér. A, 6).
  • Destouches-Février, Paulette, 1945a, “Rapports entre le calcul des problèmes et le calcul des propositions”, Comptes Rendus de l’Académie des sciences, 220: 484–486. [Destouches-Février 1945a available online]
  • –––, 1945b, “Logique adaptee aux théories quantiques”, Comptes Rendus de l’Académie des sciences, 221: 287–288. [Destouches-Février 1945b available online]
  • –––, 1947a, “Sur la notion d’adequation et le calcul minimal de Johannsson”, Comptes Rendus de l’Académie des sciences, 224: 545–547. [Destouches-Février 1947a available online]
  • –––, 1947b, “Esquisse d’une mathématique intuitioniste positive”, Comptes Rendus de l’Académie des sciences, 225: 1241–1243. [Destouches-Février 1947b available online]
  • –––, 1948, “Logique de l’intuitionisme sans négation et logique de l’intuitionisme positif”, Comptes Rendus de l’Académie des sciences, 226: 38–39. [Destouches-Février 1948 available online]
  • –––, 1949, “Connexions entre les calculs des constructions, des problèmes, des propositions”, Comptes Rendus de l’Académie des sciences, 228: 31–33. [Destouches-Février 1949 available online]
  • –––, 1951, “Sur l’intuitionnisme et la conception strictement constructive”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 80–86. doi:10.1016/S1385-7258(51)50012-4
  • Došen, Kosta, 1992, “The First Axiomatization of Relevant Logic”, Journal of Philosophical Logic, 21(4): 339–356. doi:10.1007/BF00260740
  • Dummett, Michael A.E., 1973, “The Justification of Deduction”, British Academy, London. Page references to reprint in Dummett 1978: 290–318. [Dummett 1973 available online]
  • –––, 1978, Truth and Other Enigmas, Cambridge MA: Harvard University Press.
  • –––, 2000, Elements of Intuitionism, second revised edition, Oxford: Clarendon Press.
  • Ewald, William Bragg, 1996, From Kant to Hilbert: A Source Book in the Foundations of Mathematics, 2 vols, Oxford: Oxford University Press.
  • Fitting, Melvin Chris, 1969, Intuitionistic Logic, Model Theory and Forcing, (Studies in Logic and the Foundations of Mathematics, 54), Amsterdam: North-Holland.
  • Fraenkel, Abraham A., Yehoshua Bar-Hillel, and Azriel Levy, 1973, Foundations of Set Theory, second revised edition, (Studies in Logic and the Foundations of Mathematics, 67), Amsterdam: North-Holland. The revision of the chapter on intuitionism (4) was done by Dirk van Dalen.
  • Franchella, Miriam, 1994a, “Heyting’s contribution to the change in research into the foundations of mathematics”, History and Philosophy of Logic, 15(2): 149–172. doi:10.1080/01445349408837229
  • –––, 1994b, “Brouwer and Griss on intuitionistic negation”, Modern Logic, 4(3): 256–265. [Franchella 1994b available online]
  • –––, 1995, “L.E.J. Brouwer towards intuitionistic logic”, Historia Mathematica, 22(3): 304–322. doi:10.1006/hmat.1995.1026
  • –––, 2008, Con gli occhi negli occhi di Brouwer, Monza: Polimetrica.
  • Freudenthal, Hans, 1937a, “Zum intuitionistischen Raumbegriff”, Compositio Mathematica, 4: 82–111. [Freudenthal 1937a available online]
  • –––, 1937b, “Zur intuitionistischen Deutung logischer Formeln”, Compositio Mathematica, 4: 112–116. [Freudenthal 1937b available online]
  • –––, 1937c, “Nachwort”, Compositio Mathematica, 4: 118. [Freudenthal 1937c available online]
  • –––, 1973, Mathematics as an Educational Task, Dordrecht:Reidel.
  • Gentzen, Gerhard, 1934, “Untersuchungen über das logische Schliessen”, Mathematische Zeitschrift, 39: 176–210, 405–431. English translation in Gentzen 1969: 68–131. doi:10.1007/BF01201353
  • –––, 1969, The Collected Papers of Gerhard Gentzen, M.E. Szabo (ed. and trans.), Amsterdam: North-Holland.
  • Georgacarakos, G.N., 1982, “The Semantics of Minimal Intuitionism”, Logique et Analyse, 25(100): 383–397. [Georgacarakos 1982 available online]
  • Gilmore, P.C., 1953a, “The effect of Griss’ criticism of the intuitionistic logic on deductive theories formalized within the intuitionistic logic. I”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 56: 162–174. Also Indagationes Mathematicae, 15: 162–174. doi:10.1016/S1385-7258(53)50022-8
  • –––, 1953b, “The effect of Griss’ criticism of the intuitionistic logic on deductive theories formalized within the intuitionistic logic. II”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 56: 175–186. Also Indagationes Mathematicae, 15: 175–186. doi:10.1016/S1385-7258(53)50023-X
  • –––, 1953c, “Griss’ criticism of the intuitionistic logic and the theory of order”, Proceedings of the 11th International Congress of Philosophy, Brussels 1953, Amsterdam: North-Holland, 5: 98–104.
  • –––, 1956, “Mathématique stable et Mathématique affirmative, by D. van Dantzig”, Journal of Symbolic Logic, 21(3): 323–324. doi:10.2307/2269134
  • Glivenko, V., 1928, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 14: 225–228.
  • –––, 1929, “Sur quelques points de la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 5(15): 183–188. English translation in Mancosu 1998: 301–305.
  • Gödel, Kurt, 1932, “Zum intuitionistischen Aussagenkalkül”, Anzeiger der Akademie der Wissenschaften in Wien, 69: 65–66. Also, with English translation, in Gödel 1986: 222–225.
  • –––, 1932f, “Heyting, Arend: Die intuitionistische Grundlegung der Mathematik”, Zentralblatt für Mathematik und ihre Grenzgebiete, 2: 321–322. Also, with English translation, in Gödel 1986: 246–247.
  • –––, 1933e, “Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38. Also, with English translation, in Gödel 1986: 286–295.
  • –––, 1933f, “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse eines mathematischen Kolloquiums, 4: 39–40. Also, with English translation, in Gödel 1986: 300–303.
  • –––, *1933o, “The present situation in the foundations of mathematics”, text of a lecture in Cambridge, MA, in Gödel 1995: 45–53.
  • –––, *1941, “In what sense is intuitionistic logic constructive?”, text of a lecture at Yale, in Gödel 1995: 189–200.
  • –––, 1958, “Über eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes”, Dialectica, 12(3–4): 280–287. Also, with English translation, in Gödel 1990: 240–251. doi:10.1111/j.1746-8361.1958.tb01464.x
  • –––, 1970, “On an extension of finitary mathematics which has not yet been used”, Circulated earlier version of Gödel 1972.
  • –––, 1972, “On an extension of finitary mathematics which has not yet been used”, Revised and expanded translation of Gödel 1958, first published in Gödel 1990: 271–280.
  • –––, 1986–, Collected Works, Solomon Feferman et al. (eds.), Oxford: Oxford University Press.
    • –––, 1986, I: Publications 1929–1936
    • –––, 1990, II: Publications 1938–1974
    • –––, 1995, III: Unpublished Essays and Lectures
    • –––, 2003a, IV: Correspondence A–G
    • –––, 2003b, V: Correspondence H–Z
  • Griss, G.F.C., 1944, “Negatieloze intuitïonistische wiskunde”, Verslagen Nederlandse Akademie van Wetenschappen Amsterdam, 53: 261–268.
  • –––, 1946, “Negationless intuitionistic mathematics”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 49: 1127–1133. Also Indagationes Mathematicae, 8: 675–681.
  • –––, 1947, Idealistische Filosofie, Arnhem: Van Loghum Slaterus.
  • –––, 1948a, “Sur la négation (dans les mathématiques et la logique)”, Synthese, 7(1/2): 71–74.
  • –––, 1948b, “Logique des mathématiques intuitionistes sans négation”, Comptes Rendus de l’Académie des sciences, 227: 946–948. [Griss 1948b available online]
  • –––, 1950, “Negationless intuitionistic mathematics. II”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 53: 456–463. Also Indagationes Mathematicae, 12: 108–115.
  • –––, 1951a, “Negationless Intuitionistic Mathematics. III”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 193–199. Also Indagationes Mathematicae, 13: 193–199. doi:10.1016/S1385-7258(51)50027-6
  • –––, 1951b, “Negationless Intuitionistic Mathematics. IVa”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 452–462. Also Indagationes Mathematicae, 13: 452–462. doi:10.1016/S1385-7258(51)50064-1
  • –––, 1951c, “Negationless Intuitionistic Mathematics. IVb”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 463–471. Also Indagationes Mathematicae, 13: 463–471. doi:10.1016/S1385-7258(51)50065-3
  • –––, 1951d, “Logic of Negationless Intuitionistic Mathematics”, Proceedings Koninklijke Nederlandse Akademie van Wetenschappen Amsterdam, 54: 41–49. Also Indagationes Mathematicae, 13: 41–49. doi:10.1016/S1385-7258(51)50007-0
  • van Heijenoort, Jean (ed.), 1967, From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879–1931, Cambridge, MA: Harvard University Press.
  • Hazen, A.P., 1995, “Is Even Minimal Negation Constructive?”, Analysis, 55(2): 105–107. doi:10.1093/analys/55.2.105
  • Herbrand, Jacques, 1931, “Sur la non-contradiction de l’arithmétique”, Journal für die reine und angewandte Mathematik, 166: 1–8. Also Herbrand 1968: 221–232. English translation in van Heijenoort 1967: 620–628, reprint in Herbrand 1971: 284–297.
  • –––, 1968, Écrits logiques, Jean van Heijenoort (ed.), Paris: Presses Unversitaires de France.
  • –––, 1971, Logical Writings, Warren D. Goldfarb (ed.), Cambridge, MA: Harvard University Press.
  • Hesseling, Dennis E., 2003, Gnomes in the Fog. The Reception of Brouwer’s Intuitionism in the 1920s, Basel: Birkhäuser.
  • Heyting, Arend, 1925, Intuïtionistische axiomatiek der projectieve meetkunde, Ph.D. thesis, Universiteit van Amsterdam.
  • –––, 1928, [Prize essay on the formalization of intuitionistic logic]. Expanded and revised version published as Heyting 1930, Heyting 1930A, Heyting 1930B.
    • –––, 1930, “Die formalen Regeln der intuitionistischen Logik I”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 42–56. English translation in Mancosu 1998: 311–327.
    • –––, 1930A, “Die formalen Regeln der intuitionistischen Logik II”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 57–71.
    • –––, 1930B, “Die formalen Regeln der intuitionistischen Logik III”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 158–169.
  • –––, 1930C, “Sur la logique intuitionniste”, Académie Royale de Belgique, Bulletin de la Classe des Sciences, 16: 957–963. English translation in Mancosu 1998: 306–310.
  • –––, 1931, “Die intuitionistische Grundlegung der Mathematik” (The Intuitionist Foundations of Mathematics), Erkenntnis, 2: 106–115. English translation in Benacerraf & Putnam 1983: 52–61. doi:10.1017/CBO9781139171519.003 and doi:10.1007/BF02028143
  • –––, 1932, “A propos d’un article de MM. Barzin et Errera”, Enseignement Mathématique, 31: 121–122.
  • –––, 1932C, “Anwendung der intuitionistischen Logik auf die Definition der Vollständigkeit eines Kalküls”, in Verhandlungen des Internationalen Mathematikerkongresses Zürich 1932, W. Saxer (ed.), Zürich: Orell Füssli, vol. 2, 344–345.
  • –––, 1934, Mathematische Grundlagenforschung, Intuitionismus, Beweistheorie, Berlin: Springer.
  • –––, 1937, “Bemerkungen zu dem Aufsatz von Herrn Freudenthal ‘Zur intuitionistischen Deutung logischer Formeln’”, Compositio Mathematica, 4: 117–118. [Heyting 1937c available online]
  • –––, 1955, Les fondements des mathématiques. Intuitionnisme. Théorie de la démonstration, Paris: Gauthier-Villars. Updated version of Heyting 1934, translated into French by P. Destouches-Février.
  • –––, 1953–1955, “G. F. C. Griss and His Negationless Intuitionistic Mathematics” Synthese, 9: 91–96. doi:10.1007/BF00567395
  • –––, 1956, Intuitionism, an Introduction, Amsterdam: North–Holland.
  • –––, 1958A, “Blick von der intuitionistischen Warte”, Dialectica, 12(3–4): 332–345. doi:10.1111/j.1746-8361.1958.tb01468.x
  • –––, 1958C, “Intuitionism in Mathematics”, in La philosophie au milieu du vingtième siècle, Raymond Klibansky (ed.), Firenze: La nuova Italia, vol. 1, 101–115.
  • –––, 1968A, “L.E.J. Brouwer”, in Logic and Foundations of Mathematics, (Contemporary Philosophy. A Survey, Vol.1), Raymond Klibansky (ed.), Firenze: La Nuova Italia editrice, 308–315.
  • –––, 1974, “Intuitionistic views on the nature of mathematics”, Synthese, 27(1–2): 79–91. doi:10.1007/BF00660890
  • –––, 1978, “History of the Foundations of Mathematics”, Nieuw Archief voor Wiskunde, 3rd series, 26(3): 1–21.
  • Hilbert, David, 1900, “Mathematische Probleme. Vortrag, gehalten auf dem internationalen Mathematiker-Kongress zu Paris 1900” (Mathematical Problems), Archiv der Mathematik und Physik (3), 1: 44–63,213–237. English translation in the Bulletin of the American Mathematical Society, 8(10): 437–479, 1902. doi:10.1090/S0002-9904-1902-00923-3
  • –––, 1922, “Neubegründung der Mathematik (Erste Mitteilung)”, Abhandlungen aus dem Mathematischen Seminar der Hamburgischen Universität, 1: 157–177. English translation in Mancosu 1998: 198–214.
  • –––, 1923, “Die logischen Grundlagen der Mathematik”, Mathematische Annalen, 88(1–2): 151–165. English translation in Ewald 1996: 1134–1148. doi:10.1007/BF01448445
  • Hilbert, D. and W. Ackermann, 1928, Grundzüge der theoretischen Logik, Berlin: Springer. doi:10.1007/978-3-642-52789-0
  • Imai, Yasuyuki and Kiyoshi Iseki, 1966, “On Griss Algebra. I”, Proceedings of the Japan Academy, 42(3): 213–216. doi:10.3792/pja/1195522077
  • de Iongh, J.J., 1949, “Restricted Forms of Intuitionistic Mathematics”, Proceedings of the 10th International Congress of Philosophy, Amsterdam 1948, Amsterdam: North-Holland, 2: 744–748. doi:10.5840/wcp1019492207
  • Johansson, Ingebrigt, 1937, “Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus”, Compositio Mathematica, 4: 119–136. [Johansson 1937 available online]
  • Joosten, Joost Johannes, 2004, Interpretability Formalized, Ph.D. thesis, Utrecht University. Quaestiones Infinitae vol. XLIX, [Joosten 2004 available from Universiteit Utrecht/Universiteitsbibliotheek].
  • Kennedy, Juliette, 2007, “Kurt Gödel”, in The Stanford Encyclopedia of Philosophy, Winter 2007 Edition, Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/archives/win2007/entries/goedel/>.
  • Kleene, Stephen Cole, 1945, “On the Interpretation of Intuitionistic Number Theory”, Journal of Symbolic Logic, 10(4): 109–124. doi:10.2307/2269016
  • –––, 1952, Introduction to Metamathematics, Amsterdam: North-Holland.
  • –––, 1973, “Realisability: A Retrospective Survey”, in Mathias & Rodgers 1973: 95–112. doi:10.1007/BFb0066772
  • Kleene, Stephen Cole and Richard Eugene Vesley, 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, (Studies in logic and the foundations of mathematics, 39), Amsterdam: North-Holland.
  • Kolmogorov, A., 1925, “O principe tertium non datur”, Matematiceskij Sbornik, 32: 646–667. English translation in van Heijenoort 1967: 416–437.
  • –––, 1932, “Zur Deutung der Intuitionistischen Logik”, Mathematische Zeitschrift, 35: 58–65. English translation in Mancosu 1998: 328–334. doi:10.1007/BF01186549
  • –––, 1937, “Freudenthal, Hans: Zur intuitionistischen Deutung logischer Formeln. Heyting, A.: Bemerkungen zu dem Aufsatz von Herrn Freudenthal ‘Zur intuitionistischen Deutung logischer Formeln’”, Zentralblatt für Mathematik und ihre Grenzgebiete, 0015.24201 [Photocopy/scan of Kolmogorov 1937 available online].
  • Korevaar, Jaap., 2016, “Enkele persoonlijke herinneringen aan L.E.J. Brouwer”, (“Some personal memories of L.E.J. Brouwer”), Nieuw Archief voor Wiskunde, 5th series, 17(4): 247–249. [Korevaar 2016 available online]
  • Kreisel, G., 1962, “Foundations of Intuitionistic Logic”, in Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress, Ernst Nagel, Patrick Suppes, and Alfred Tarski (eds.), Stanford: Stanford University Press, 198–210. doi:10.1016/S0049-237X(09)70587-7
  • –––, 1987, “Gödel’s Excursions into Intuitionistic Logic”, in Gödel Remembered, P. Weingartner and L. Schmetterer (eds.), Napoli: Bibliopolis, 67–179.
  • Kripke, Saul A., 1965, “Semantical Analysis of Intuitionistic Logic I”, in Formal Systems and Recursive Functions, (Studies in Logic and the Foundations of Mathematics, 40), J.N. Crossley and M. Dummett (eds.), Amsterdam: North-Holland, 92–130. doi:10.1016/S0049-237X(08)71685-9
  • Krivtsov, Victor N., 2000a, “A Negationless Interpretation of Intuitionistic Theories”, Erkenntnis, 53(1–2): 155–172. doi:10.1023/A:1005618302941
  • –––, 2000b, “A Negationless Interpretation of Intuitionistic Theories. I”, Studia Logica, 64(3): 323–344. doi:10.1023/A:1005233526469
  • –––, 2000c, “A Negationless Interpretation of Intuitionistic Theories. II”, Studia Logica, 65(2): 155–179. doi:10.1023/A:1005207512630
  • Kuiper, Johannes John Carel, 2004, Ideas and Explorations. Brouwer’s Road to Intuitionism, Ph.D. thesis, Utrecht University. Quaestiones Infinitae vol. XLVI [Kuiper 2004 available from Universiteit Utrecht/Universiteitsbibliotheek].
  • Lewis, C.I., 1914, “The Calculus of Strict Implication”, Mind, New Series, 23(90): 240–247. doi:10.1093/mind/XXIII.1.240
  • Mancosu, Paolo (ed.), 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press.
  • Mathias, A.R.D. and H. Rodgers (eds.), 1973, Cambridge Summer School in Mathematical Logic 1971, (Lecture Notes in Mathematics, 337), Heidelberg: Springer. doi:10.1007/BFb0066770
  • McKinsey, J.C.C., 1939, “Proof of the Independence of the Primitive Symbols of Heyting’s Calculus of Propositions”, Journal of Symbolic Logic, 4(4): 155–158. doi:10.2307/2268715
  • Mendez, José M., 1988, “A Note on the Semantics of Minimal Intuitionism”, Logique et Analyse, 31(123–124): 371–377. [Mendez 1988 available online]
  • Michel, David, 2008, Systèmes formels et systèmes fonctionnels pédagogiques, Ph.D. thesis, Université Metz. [Michel 2008 available from Université de Lorraine].
  • Mints, Grigori, 2006, “Notes on Constructive Negation”, Synthese, 148(3): 701–717. doi:10.1007/s11229-004-6294-3
  • van der Molen, Tim, 2016, “The Johansson/Heyting letters and the birth of minimal logic”, ILLC Publications, Technical Notes Series, X-2016-04 [van der Molen 2016 available online from ILLC].
  • Moschovakis, Joan, 2007, “Intuitionistic Logic”, in The Stanford Encyclopedia of Philosophy, Spring 2007 Edition, Edward N. Zalta (ed.), URL=<https://plato.stanford.edu/archives/spr2007/entries/logic-intuitionistic/>.
  • Myhill, John, 1966, “Notes Towards An Axiomatization of Intuitionistic Analysis”, Logique et Analyse, 9(35–36): 280–297. [Myhill 1966 available online]
  • Nelson, David, 1966, “Non-Null Implication”, Journal of Symbolic Logic, 31(4): 562–572. doi:10.2307/2269691
  • Parsons, Charles, 1967, [Introduction to the translation of sections 1–3 of Brouwer 1927B], in van Heijenoort 1967: 446–457.
  • Pieri, Mario, 1898, “I principii della geometria di posizione composti in sistema logico deduttivo”, Memorie della Reale Accademia delle Scienze di Torino, series II, 48: 1–62.
  • Plisko, V.E., 1988, “The Kolmogorov calculus as a part of minimal calculus”, Russian Mathematical Surveys, 43(6): 95–110. doi:10.1070/RM1988v043n06ABEH001993
  • Pos, H.J., 1953–1954, “G.F.C. Griss als wijsgerig humanist en als mens”, De Nieuwe Stem, 8: 654–663.
  • Posy, Carl J., 1992, “Review: Dirk van Dalen, Intuitionistic Logic; Walter Felscher, Dialogues as a Foundation for Intuitionistic Logic”, Journal of Symbolic Logic, 57(2): 754–756. doi:10.2307/2275309
  • Prawitz, Dag, 1965, Natural Deduction. A Proof-Theoretical Study, Stockholm: Almqvist & Wiksell.
  • Prawitz, D. and P.-E. Malmnäs, 1968, “A Survey of Some Connections Between Classical, Intuitionistic and Minimal Logic”, in Contributions to Mathematical Logic, (Studies in Logic and the Foundations of Mathematics, 50), H. Arnold Schmidt, K. Schütte, and H.-J. Thiele (eds.), Amsterdam: North-Holland, pp. 215–229. doi:10.1016/S0049-237X(08)70527-5
  • Rasiowa, Helena, 1974, An Algebraic Approach to Non-Classical Logics, (Studies in logic and the foundations of mathematics, 78), Amsterdam: North-Holland/
  • Ruitenburg, Wim, 1991, “The Unintended Interpretations of Intuitionistic Logic”, in Perspectives on the History of Mathematical Logic, Thomas Drucker (ed.), Basel: Birkhäuser, 134–160. doi:10.1007/978-0-8176-4769-8_10
  • van Rootselaar, B., 1953–1954, “In memoriam Dr. G.F.C. Griss”, Euclides, 29(1): 42–45.
  • Russell, Bertrand, 1903, The Principles of Mathematics, London: Allen & Unwin.
  • Sato, Masahiko, 1997, “Classical Brouwer-Heyting-Kolmogorov interpretation”, RIMS Kokyuroku, 1021: 28–47.
  • Smirnov, V.J., 1925 [published 1932], “Kolmogorov, A.N.: Über das Prinzip tertium non datur”, Jahrbuch über die Fortschritte der Mathematik 51.0048.01.
  • van Stigt, Walter P., 1990, Brouwer’s Intuitionism, (Studies in the history and philosophy of mathematics, 2), Amsterdam: North-Holland.
  • Stone, Marshall Harvey, 1937, “Topological Representations of Distributive Lattices and Brouwerian Logics”, Časopis pro pěstování matematiky a fysiky, 67(1): 1–25.
  • Sundholm, Göran, 1983, “Constructions, Proofs and the Meaning of Logical Constants”, Journal of Philosophical Logic, 12(2): 151–172. doi:10.1007/BF00247187
  • –––, 2004, “The Proof-Explanation of Logical Constants is Logically Neutral”, Revue Internationale de Philosophie, 58(4): 401–410.
  • Sundholm, Göran and Mark van Atten, 2008, “The proper explanation of intuitionistic logic: on Brouwer’s proof of the Bar Theorem”, in van Atten et al. 2008: 60–77. doi:10.1007/978-3-7643-8653-5_5
  • de Swart, H.C.M., 1976, “Another Intuitionistic Completeness Proof”, Journal of Symbolic Logic, 41(3): 644–662. doi:10.1017/S0022481200051215
  • –––, 1977, “An Intuitionistically Plausible Interpretation of Intuitionistic Logic”, Journal of Symbolic Logic, 42(4): 564–578. doi:10.2307/2271877
  • Tarski, Alfred, 1938, “Der Aussagenkalkül und die Topologie”, Fundamentae Mathematicae, 31: 103–134. English translation in Tarski 1956, pp. 421–454.
  • –––, 1953, “A General Method in Proofs of Undecidability”, in Undecidable Theories, A. Tarski, A. Mostowski, and R. Robinson (eds.), Amsterdam: North-Holland, 3–35.
  • –––, 1956, Logic, Semantics, Metamathematics. Papers from 1923 to 1938, J.H. Woodger (trl.), Clarendon Press.
  • Troelstra, A.S., 1977, “Aspects of constructive mathematics”, in Handbook of Mathematical Logic, (Studies in Logic and the Foundations of Mathematics, 90), Jon Barwise (ed.), Amsterdam: North-Holland, 973–1052. doi:10.1016/S0049-237X(08)71127-3
  • –––, 1983, “Logic in the Writings of Brouwer and Heyting”, in Atti del Convegne Internazionaledi Storia della Logica. San Gimignano, 4–8 dicembre 1982, V. Abrusci, E. Casari, and M. Mugnai, eds., Bologna: CLUEB, 193–210.
  • –––, 1990, “On the Early History of Intuitionistic Logic”, in Mathematical Logic, Petio P. Petkov (ed.), New York: Plenum Press, 3–17.
  • Troelstra, A.S., J. Niekus, and H. van Riemsdijk, 1981, “Bibliography of A. Heyting”, Nieuw Archief voor Wiskunde, 3rd series, 29: 24–35.
  • Troelstra, A.S. and D. van Dalen, 1988, Constructivism in Mathematics, 2 vols., (Studies in Logic and the Foundations of Mathematics, 121 & 123), Amsterdam: North-Holland.
  • Valpola, Veli, 1955, “Ein system der negationlosen Logik mit ausschliesslich realisierbaren Prädicaten”, Acta Philosophica Fennica, 9: 1–247.
  • Veldman, Wim, 1976, “An Intuitionstic Completeness Theorem for Intuitionistic Predicate Logic”, Journal of Symbolic Logic, 41(1): 159–166. doi:10.1017/S0022481200051859
  • –––, 1982, “On the Continuity of Functions in Intuitionistic Real Analysis. Some Remarks on Brouwer’s Paper: ‘Ueber Definitionsbereiche von Funktionen’”, Tech. Rep. 8210, Mathematisch Instituut, Katholieke Universiteit Nijmegen.
  • –––, 2008, “The Borel Hierarchy Theorem from Brouwer’s Intuitionistic Perspective”, Journal of Symbolic Logic, 73(1): 1–64. doi:10.2178/jsl/1208358742
  • Vesley, Richard, 1980, “Intuitionistic Analysis: the Search for Axiomatization and Understanding”, in The Kleene Symposium, (Studies in Logic and the Foundations of Mathematics, 101), J. Barwise, H. J. Keisler, and K. Kunen (eds.), Amsterdam: North-Holland, 317–331. doi:10.1016/S0049-237X(08)71265-5
  • Vredenduin, P.G.J., 1953, “The Logic of Negationless Mathematics”, Compositio Mathematica, 11: 204–277. [Vredenduin 1953 available online]
  • –––, 1956, “G.F.C. Griss and his Negationaless Intuitionistic Mathematics, by A. Heyting”, Journal of Symbolic Logic, 21(1): 91. doi:10.2307/2268511
  • Wajsberg, Mordchaj, 1938, “Untersuchungen über den Aussagenkalkül [von A. Heyting]”, Wiadomosci Matematyczne, (old series) 46: 45–101.
  • Wang, Hao, 1987, Reflections on Kurt Gödel, Cambridge MA: MIT Press.
  • Wavre, Rolin, 1924, “Y a-t-il une crise des mathématiques? A propos de la notion d’existence et d’une application suspecte du principe du tiers exclu”, Revue de Métaphysique et de Morale, 31(3) 435–470.
  • –––, 1926, “Logique formelle et logique empirique”, Revue de Métaphysique et de Morale, 33(1): 65–75.
  • Weyl, Hermann, 1921, “Über die neue Grundlagenkrise der Mathematik”, Mathematische Zeitschrift, 10(1–2): 39–79. English translation in Mancosu 1998: 86–118. doi:10.1007/BF02102305
  • Whitehead, Alfred North, 1906, The Axioms of Projective Geometry, Cambridge: Cambridge University Press.
  • Whitehead, Alfred North and Bertrand Russell, 1910, Principia Mathematica, vol. 1, Cambridge: Cambridge University Press.

Acknowledgments

I am grateful to Dirk van Dalen and Göran Sundholm for discussions of some of the issues involved. Helpful comments by the editors and Rosalie Iemhoff led to various improved formulations, corrections, and clarifications. Van Dalen kindly granted permission to quote from materials in the Brouwer Archive (at Utrecht at the time, now at the Noord-Hollands Archief in Haarlem). Thanks also to van Dalen and Eckhart Menzler-Trott for their search for Bernays’ letter to Brouwer, and to Sundholm and Michael Hegarty for a copy of de Iongh 1949. In section 3.6 I have drawn on van Atten 2004a; I thank the Association for Symbolic Logic for granting permission to do so.

Copyright © 2017 by
Mark van Atten <vanattenmark@gmail.com>

This is a file in the archives of the Stanford Encyclopedia of Philosophy.
Please note that some links may no longer be functional.
[an error occurred while processing the directive]