The Development of Intuitionistic Logic

First published Thu Jul 10, 2008; substantive revision Wed Apr 1, 2009

We will be principally concerned with the historical development of the intuitionists’ explanation of the logical connectives. An “explanation” here is an account of what one knows when one understands and correctly uses the logical connectives. The emphasis is on (the history of) Brouwer's explanation of logic within the framework of intuitionistic mathematics, and on (the history of) its codification in Heyting's Proof Interpretation.

In future updates of this entry, the following topics will be added: (a) precursors to Brouwer, (b) early objections to the Proof Interpretation, and (c) later developments around the Proof Interpretation.

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 and van Dalen 1988, 9):

(H1) A proof of A ∧ B is given by presenting a proof of A and a proof of B.
(H2) A proof of A ∨ 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 ∨ B).
(H3) A proof of A → B is a construction which permits us to transform any proof of A into a proof of B.
(H4) Absurdity ⊥ (contradiction) has no proof; a proof of ¬A is a construction which transforms any hypothetical proof of A into a proof of a contradiction.
(H5) A proof of ∀xA(x) is a construction which transforms a proof of d ∈ D (D the intended range of the variable x) into a proof of A(d).
(H6) A proof of ∃xA(x) is given by providing d ∈ 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 and van Dalen 1988, 9, 32–33).[1] 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 ¬∀x(Px ∨ ¬Px), while classically there can be none (see the section on Strong counterexamples and the Creating Subject, 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.[2] 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:[3]

If U ⊢ A then V ⊢ 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 (1977a, 977), where “K” initially stood for “Kreisel” (because of Kreisel 1962a), later for “Kolmogorov”, e.g., in Troelstra 1990 (p.6); in a future update of this entry, it will be explained that 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 Brouwer 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)/(Brouwer 1975, 61, n.1).[4] The point of departure for these constructions is the intuition of the flow of time.[5] 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)/(Brouwer 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)/(Brouwer 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)/(Brouwer 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 the weather-map accompanies the atmospheric processes” (Brouwer 1975, 451). 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)/(Brouwer 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)/(Brouwer 1975, 443). 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)/(Brouwer 1975, 72–75, 88), but a more memorable passage is in the paper from 1908:

Is it allowed, in purely mathematical constructions and transformations, to neglect for some time the idea of the mathematical system under construction and to operate in the corresponding linguistic structure, following the principles of syllogism, of contradiction and of tertium exclusum, and can we then have confidence that each part of the argument can be justified by recalling to the mind the corresponding mathematical construction? (Brouwer 1908, 4)/(Brouwer 1975, 109)

(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 Princple 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)/(Brouwer 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 (p.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 (Brouwer 1907, 125–128)/(Brouwer 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)/(Brouwer 1975, 72 (modified))

Different readings of this concise passage have been proposed. According to one, Brouwer's passage bears on A → B in the following way:

(α) 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 α, A → B just means A ∧ B with the extra information that the construction for B was obtained from that for A. On this reading A → 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 we will see in a future update of this entry, Freudenthal (1936) too has suggested this strategy, albeit with a different motivation.) 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 β:

(β) In order to establish A → 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 in press)

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.

On either reading, it is clear that Brouwer had the Proof Interpretation of the implication in mind already in 1907; for on either reading, the essential component in the explanation of A → B is the preservation of constructibility from A to B. 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 in press, 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 ¬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)/(Brouwer 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 → 1=2 (Brouwer 1954A, 3). In practice, one defines ¬A := A → 1=2 (and hence ¬1=2 is seen as a particular case of A → 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 ¬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 1908; see also Brouwer 1949A (p. 1243).

In that paper, Brouwer draws a consequence of his general view on logic that he had overlooked in his dissertation: PEM, A ∨ ¬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 π a digit which occurs more often than any other one?
Do there occur in the decimal expansion of π infinitely many pairs of consecutive equal digits? (Brouwer 1908, 7)/(Brouwer 1975, 110)

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 (Brouwer 1921A, Brouwer 1924N, Brouwer 1925E).

Brouwer remarks in the 1908 paper that the fact that PEM is not valid does not mean that it is false: ¬(A ∨ ¬ A) implies ¬A ∧ ¬¬A, a contradiction. In other words, ¬¬(A ∨ ¬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 1908, 7n.2)/(Brouwer 1975, 110n.2). 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 1908 but that of Brouwer 1955). So on these grounds A ∨ ¬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 ∨ ¬A as ¬A → ¬A (Brouwer 1907, 131, 160)/(Brouwer 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)/(Brouwer 1975, 101); this principle is the constructively correct reading of PEM. In the paper from 1908, he corrected his earlier understanding of PEM:

Now consider the principium tertii exculsi: it claims that every supposition is either true or false; in mathematics this means that for every supposed embedding of a system into another, satisfying certain conditions, we can either accomplish such an embedding by a construction, or we can arrive by a construction at the arrestment of the process which would lead to the embedding. (Brouwer 1908, 5)/(Brouwer 1975, 109)

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 1900b] 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 ∨ ¬A, the latter to ¬¬(A ∨ ¬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 2001, 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 ¬¬(A ∨ ¬A) means that no absolutely unsolvable problem can be indicated was made in Heyting 1934 (p. 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 ¬¬¬A ⇔ ¬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 → B implies that ¬B → ¬A (because ¬B is B → ⊥ and → is transitive). 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 → B would lead to a proof of B and thereby make it impossible to begin establishing the second implication by proving its antecedent ¬B.

Later, Brouwer pointed out the following consequence of the validity of ¬¬¬A ⇔ ¬A: the proof method of reductio ad absurdum, which is not generally correct (not “reliable”) intuitionistically, can be used to establish negative propositions ¬A (Brouwer 1929A, 163)/(Mancosu 1998, 52). For if the assumption of ¬¬A leads to a contradiction, that is, to ¬¬¬A, the equivalence allows one to simplify that to ¬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, Brouwer 1927B, Brouwer 1954A). This is evidently not the same as an implication A → 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 → 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 < is virtual if it satisfies the following axioms (Brouwer 1926A, 453):

  1. The relations r = s, r < s and r > s are mutually exclusive.
  2. From r = u, s = v and r < s follows u < v.
  3. From the simultaneous failure of the relations r > s and r = s follows r < s.
  4. From the simultaneous failure of the relations r > s and r < s follows r = s.
  5. From r < s and s < t follows r < 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 π. 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 ∃xP(x) nor ∀x¬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 R stands for the set of intuitionistic real numbers, and 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. ∀x ∈ R(x ∈ Q ∨ x ∉ Q) (Brouwer 1925E)
  5. Any two straight lines in the Euclidian 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:

¬∀x∈R(x ∈ Q ∨ x ∉ 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] → 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,

  • ¬∀x∈R(¬¬ x > 0 → x > 0) (Brouwer 1949A)
  • ¬∀x∈R(x ≠ 0 → x < 0 ∨ x > 0) (Brouwer 1949B)

As the actual arguments using these methods quickly get somewhat complicated, but introduce no new logical phenomena as such — weak and strong counterexamples can also be given by other means — we refer to the literature for further details: Brouwer 1949A, Brouwer 1949B, Brouwer 1954F; Heyting 1956 (pp. 117–120); Myhill 1968; Dummett 2000a (pp. 244–245). 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 must be 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 α may be in at any particular moment are made explicit:

  1. α has been proved to be true;
  2. α has been proved to be false, i.e. absurd;
  3. α has neither been proved to be true nor to be absurd, but an algorithm is known leading to a decision either that α is true or that α is absurd;
  4. α has neither been proved to be true nor to be absurd, nor do we know an algorithm leading to the statement either that α is true or that α 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 α 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 ¬¬(A ∨ ¬ 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 ¬¬A → 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)/(Brouwer 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 (p. 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 2003, 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 logic, which for him was a form of applied mathematics, he never made an extensive study of the latter, and in particular never made a systematic comparison between on the one hand intuitionistic logic and on the other hand classical logic as formalized, for example, in Principia Mathematica (Whitehead and Russell 1910) or by the Hilbert school (Hilbert 1923,Hilbert and 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 ¬¬a ⊃ 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 (Brouwer 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 Royal Academy of Sciences (Brouwer 1918B, Brouwer 1919A, Brouwer 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 B (presumably for “Brouwer”) is:

  1. A → (B → A)
  2. (A → (A → B)) → (A → B)
  3. (A → (B → C)) → (B → (A → C))
  4. (B → C) → ((A → B) → (A → C))
  5. (A → B) → ((A → ¬B) → ¬A)

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

6. ¬¬A → A

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

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

A* = ¬¬A for atomic A
F(φ1, φ2,… ,φk)* = ¬¬F(φ1*, φ2*, … ,φk*) for composed formulas

and proves this interpretability result:

If U ⊢H φ then U* ⊢B φ*

where U is a set of axioms of H, and U* the set of its translations (which Kolmogorov shows to be derivable in 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 → 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 π, then 3.1 is an initial segment of π”. It also indicates an incoherence in Kolmogorov's position: one cannot at the same time accept A → (B → A) as an axiom and deny that anything can be asserted about the consequences of an impossible B.

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:

  1. p → p
  2. (p → q) → ((q → r) → (p → r))
  3. (p ∧ q) → p
  4. (p ∧ q) → q
  5. (r → p) → ((r → q) → (r → (p ∧ q)))
  6. p → (p ∨ q)
  7. q → (p ∨ q)
  8. (p → r) → ((q → r) → ((p ∨ q) → r))
  9. (p → q) → ((p → ¬ q) → ¬ p)

From these axioms, he then proved

  1. ¬¬(p ∨ ¬p)
  2. ¬¬¬p → ¬p
  3. ((¬p ∨ p) → ¬q) → ¬q

The first two had already informally been argued for by Brouwer (Brouwer 1908, Brouwer 1925E); the third was new. Now suppose that in intuitionistic logic, a proposition may be true (p holds), false (¬p holds), or have a third truth value (p′ holds). Clearly, p → ¬p′ and ¬p → ¬p′, and therefore (¬p ∨ p) → ¬p′; but then, by the third of the lemmata above and axiom 8 in the list, ¬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 ¬¬p is provable in intuitionistic propositional logic;
  2. If ¬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:

  1. (p → (q → r)) → (q → (p → r))
  2. (p → (p → r)) → (p → r)
  3. p → (q → p)
  4. ¬q → (q → p)

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 ∨ ¬q) → (q → 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 (p. 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 ¬¬ 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), (Heyting 1930A), (Heyting 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:

  1. a → (a ∧ a)
  2. (a ∧ b) → (b ∧ a)
  3. (a → b) → ((a ∧ c)→ (b ∧ c))
  4. ((a → b) ∧ (b → c)) → (a → c)
  5. b → (a → b)
  6. (a ∧ (a → b)) → b
  7. a → (a ∨ b)
  8. (a ∨ b) → (b ∨ a)
  9. ((a → c) ∧ (b → c)) → ((a ∨ b) → c)
  10. ¬a → (a → b)
  11. ((a → b) ∧ (a → ¬b)) → ¬a

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; this will be discussed in a future update of this entry.) 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 10 above). He was somewhat more elaborate on this point than they had been:

The formula a → 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 → b has been proved in the sense specified, it turns out that b is always correct. One accepted, the formula a → b then has to remain correct; that is, we must attribute a meaning to the sign → such that a → 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 [5] and [10] are accepted. (Heyting 1930, 44)/(Mancosu 1998, 313)

The argument is, however, incomplete. It is uncontroversial that, once a → b has been proved, it should remain so when afterward ¬ a is proved. But why should a → b, if it has not yet been proved, become provable just by establishing ¬a? (Johansson asked this in a letter to Heyting of September 23, 1935;[28] the matter will be discussed in a future update of this entry.) 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; this will be treated in a future update of this entry.) 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
    PA ⊢ A ⇔ HA ⊢ 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)/(Gödel 1986, 295). Heyting replied that “for the intuitionist, the interpretation is what is essential” (Heyting 1934,18, trl. 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)/(Gödel 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 IPC to classical modal logic S4 such that
    If IPC ⊢ A then S4 ⊢ 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 ⊢ A ∨ B, then ⊢ A or ⊢ B;
    • the Explicit Definability property (EP): if ⊢ ∃x P(x), then ⊢ 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 →, ∧, ∨, ¬ can be defined in terms of the others. Heyting had stated this in Heyting 1930 (p. 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, Gödel 1970, Gödel 1972) (which will be discussed in a future update of this entry).

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 (which will be treated in a future update of this entry).

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 (p. 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 → 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 and 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 ⊢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:

⊢¬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 ⊢p and ⊢ ¬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 ¬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:

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. [Brouwer to De Donder, October 9, 1930, trl. van Dalen 2005 (p. 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 fulfilment 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 ¬p and +¬p, as a proof of ¬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., ⊢ ¬+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, ¬p, and p ∨ 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 and 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 fulfilment 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 and Putnam 1983, 60) (modified)

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

“p ∨ 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 and 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 and 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 ¬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 → 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 → 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 → b and +a → +b. (Troelstra 1983a, 206–207) [translation mine]

This explanation of implication, which is the one that became standard, would be introduced in print only in Heyting 1934 (p. 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 1908, 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 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. (An example of such a possible occasion would be the period 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 ∧ b designates the problem “to solve both problems a and b”, while a ∨ b designates the problem “to solve at least one of the problems a and b”. Furthermore, a ⊃ 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” … ¬a designates the problem “to obtain a contradiction provided that the solution of a is given” … (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 ∨ ¬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 (pp. 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 a future update of this entry), he consistently speaks of “intention or problem” (Kolmogorov 1937). In that exchange itself, Freudenthal (1936, 119) 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 ¬a is solved, then the solution of a is impossible and the problem a → 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, ¬a → (a → 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 1900b (p. 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 ¬a ⊃ (a ⊃ 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 ¬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 ∧ q can be asserted if and only if both p and q can be asserted.”
  3. “p ∨ q can be asserted if and only if at least one of the propositions p and q can be asserted.
  4. “¬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 → 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. “⊢ (∀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. “(∃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 [¬p → (p → 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 → q can be asserted if and only if we possess a construction which, joined to the construction p, would prove q. Now suppose that ⊢ ¬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.

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

  • Artemov, S., 2001, “Explicit provability and constructive semantics”, Bulletin of Symbolic Logic, 7(1): 1–36.
  • van Atten, M., 2004a, “Review of D. Hesseling, Gnomes in the Fog. The Reception of Brouwer's Intuitionism in the 1920s”, Bulletin of Symbolic Logic, 10(3): 423–427.
  • van Atten, M., 2004b, On Brouwer, Belmont (CA): Wadsworth.
  • van Atten, M., 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.
  • van Atten, M., in press, “The hypothetical judgement in the history of intuitionistic logic”, forthcoming in Logic, Methodology, and Philosophy of Science XIII: Proceedings of the 2007 International Congress in Beijing, C. Glymour, W. Wang, and D. Westerståhl, eds., London: King's College Publications.
  • van Atten, M., Boldini, P., Bourdeau, M., and Heinzmann, G. (eds.), 2008, One Hundred Years of Intuitionism (1907–2007). The Cerisy Conference, Basel: Birkhäuser.
  • Barzin, M. and Errera, A., 1927, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 13: 56–71.
  • Bazhanov, V.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.
  • Becker, O., 1927, “Mathematische Existenz. Untersuchungen zur Logik und Ontologie mathematischer Phänomene”, Jahrbuch für Philosophie und phänomenologische Forschung, VIII: 439–809.
  • Becker, O., 1930, “Zur Logik der Modalitäten”, Jahrbuch für Philosophie und phänomenologische Forschung, XI: 497–548.
  • Benacerraf, P. and Putnam, H. (eds.), 1983, Philosophy of Mathematics: Selected Readings, 2nd ed., Cambridge: Cambridge University Press.
  • Bernays, P., 1926, “Axiomatische Untersuchung des Aussagen-Kalküls der “Principia Mathematica””, Mathematische Zeitschrift, 25: 305–320.
  • Bernays, P., 1967, “Hilbert, David”, in The Encyclopedia of Philosophy (vol. 3), P. Edwards, ed., New York: Macmillan.
  • Beth, E., 1956, “Semantic construction of intuitionistic logic”, Med. Nederl. Akad. Wet., Afd. Lett., 19(11): 357–388.
  • Brouwer, L.E.J., 1907, Over de Grondslagen der Wiskunde, Ph.D. thesis, Universiteit van Amsterdam. English translation in Brouwer 1975 pp. 11–101.
  • Brouwer, L.E.J., 1908, “De onbetrouwbaarheid der logische principes”, Tijdschrift voor Wijsbegeerte, 2: 152–158. English translation in Brouwer 1975 pp. 107–111.
  • Brouwer, L.E.J., 1918B, “Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre”, KNAW Verhandelingen, 5: 1–43.
  • Brouwer, L.E.J., 1919A, “Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Zweiter Teil, Theorie der Punktmengen”, KNAW Verhandelingen, 7: 1–33.
  • Brouwer, L.E.J., 1921A, “Besitzt jede reelle Zahl eine Dezimalbruchentwicklung?”, Mathematische Annalen, 83: 201–210. English translation in Mancosu 1998 pp. 28–35.
  • Brouwer, L.E.J., 1924D1, “Bewijs dat iedere volle functie gelijkmatig continu is”, KNAW verslagen, 33: 189–193. English translation in Mancosu 1998, pp. 36–39.
  • Brouwer, L.E.J., 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, pp. 335–341.
  • Brouwer, L.E.J., 1925E, “Intuitionistische Zerlegung mathematischer Grundbegriffe”, Jahresb. D.M.V., 33: 251–256. English translation in Mancosu 1998, pp. 287–289 (sections 2–4),290–292 (section 1).
  • Brouwer, L.E.J., 1926A, “Zur Begründung der intuitionistischen Mathematik, II”, Mathematische Annalen, 95: 453–472.
  • Brouwer, L.E.J., 1927B, “Über Definitionsbereiche von Funktionen”, Mathematische Annalen, 97: 60–75. English translation of sections 1–3 in van Heijenoort 1967, pp. 457–463.
  • Brouwer, L.E.J., 1928A2, “Intuitionistische Betrachtungen über den Formalismus”, KNAW Proceedings, 31: 374–379. English translation in Mancosu 1998, pp. 40–44.
  • Brouwer, L.E.J., 1929A, “Mathematik, Wissenschaft und Sprache”, Monatshefte für Mathematik und Physik, 36: 153–164. English translation in Mancosu 1998 pp.45–53.
  • Brouwer, L.E.J., 1930A, Die Struktur des Kontinuums, Wien: Komitee zur Veranstaltung von Gastvorträgen ausländischer Gelehrter der exakten Wissenschaften. English translation in Mancosu 1998, pp. 54–63.
  • Brouwer, L.E.J., 1933A2, “Willen, weten, spreken”, in De Uitdrukkingswijze der Wetenschap, L.E.J. Brouwer et al., Groningen: Noordhoff, 45–63. English translation in van Stigt 1990, pp. 418–431.
  • Brouwer, L.E.J., 1948A, “Essentieel negatieve eigenschappen”, Indagationes Mathematicae, 10: 322–323. English translation in Brouwer 1975, pp. 478–479.
  • Brouwer, L.E.J., 1949A, “De non-aequivalentie van de constructieve en de negatieve orderelatie in het continuum”, Indagationes Mathematicae, 11: 37–39. English translation in Brouwer 1975, pp. 495–496.
  • Brouwer, L.E.J., 1949B, “Contradictoriteit der elementaire meetkunde”, KNAW Proc., 52: 315–316. English translation in Brouwer 1975, pp. 497–498.
  • Brouwer, L.E.J., 1949C, “Consciousness, philosophy and mathematics”, Proceedings of the 10th International Congress of Philosophy, Amsterdam 1948, 3: 1235–1249.
  • Brouwer, L.E.J., 1952B, “Historical background, principles and methods of intuitionism”, South African Journal of Science, 49: 139–146.
  • Brouwer, L.E.J., 1954A, “Points and spaces”, Canadian Journal of Mathematics, 6: 1–17.
  • Brouwer, L.E.J., 1954F, “An example of contradictority in classical theory of functions”, Indag. Math., 16: 204–205.
  • Brouwer, L.E.J., 1955, “The effect of intuitionism on classical algebra of logic”, Proceedings of the Royal Irish Academy, 57: 113–116.
  • Brouwer, L.E.J., 1975, Collected Works. I: Philosophy and Foundations of Mathematics, ed. A. Heyting, Amsterdam: North-Holland.
  • Brouwer, L.E.J., 1981A, Brouwer's Cambridge Lectures on Intuitionism, Cambridge: Cambridge University Press.
  • van Dalen, D., 1973, “Lectures on intuitionism”, in Cambridge Summer School in Mathematical Logic 1971, H. Rodgers and A. Mathias, eds., Heidelberg: Springer, vol. 337 of Lecture Notes in Mathematics, 1–94.
  • van Dalen, D., 1997, “A bibliography of L.E.J. Brouwer”, Utrecht Logic Group Preprint Series, no.176 [Preprint available online]. Updated version in van Atten et al. 2008, pp. 343–390.
  • van Dalen, D., 1999, Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 1: The Dawning Revolution, Oxford: Clarendon Press.
  • van Dalen, D., 2001a, L.E.J. Brouwer 1881–1966. Een Biografie. Het Heldere Licht van de Wiskunde, Amsterdam: Bert Bakker.
  • van Dalen, D., 2001b, L.E.J. Brouwer en de Grondslagen van de Wiskunde, Utrecht: Epsilon.
  • van Dalen, D., 2004, “Kolmogorov and Brouwer on constructive implication and the Ex Falso rule”, Russian Math Surveys, 59: 247–257.
  • van Dalen, D., 2005, Mystic, Geometer, and Intuitionist. The Life of L.E.J. Brouwer. 2: Hope and Disillusion, Oxford: Clarendon Press.
  • van Dalen, D., 2008, “Another look at Brouwer's dissertation”, in van Atten et al. 2008, 3–20.
  • Došen, K., 1992, “The first axiomatization of relevant logic”, Journal of Philosophical Logic, 21: 339–356.
  • Dummett, M., 1973, “The Justification of Deduction”, British Academy, London. Page references to reprint in Dummett 1978, pp. 290–318.
  • Dummett, M., 1978, Truth and Other Enigmas, Cambridge MA: Harvard University Press.
  • Dummett, M., 2000, Elements of Intuitionism, 2nd, rev. ed., Oxford: Clarendon Press.
  • Ewald, W., 1996, From Kant to Hilbert. Readings in the Foundations of Mathematics, 2 vols, Oxford: Oxford University Press.
  • Franchella, M., 1994, “Heyting's contribution to the change in research into the foundations of mathematics”, History and Philosophy of Logic, 15(2): 149–172.
  • Franchella, M., 1995, “L.E.J. Brouwer towards intuitionistic logic”, Historia Mathematica, 22: 304–322.
  • Freudenthal, H., 1936, “Zur intuitionistischen Deutung logischer Formeln”, Compositio Mathematica, 4: 112–116.
  • Gentzen, G., 1934, “Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, 39: 176–210, 405–431. English translation in Gentzen 1969, pp. 68–131.
  • Gentzen, G., 1969, The Collected Papers of Gerhard Gentzen, ed.,trl. M. Szabo, Amsterdam: North-Holland.
  • Glivenko, V., 1928, “Sur la logique de M. Brouwer”, Académie Royale de Belgique, Bulletin de la classe des sciences, 14: 225–228.
  • Glivenko, V., 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, pp. 301–305.
  • Gödel, K., 1932, “Zum intuitionistischen Aussagenkalkül”, Anzeiger der Akademie der Wissenschaften in Wien, 69: 65–66. Also, with English translation, in Gödel 1986, pp. 222–225.
  • Gödel, K., 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, pp. 246–247.
  • Gödel, K., 1933e, “Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums, 4: 34–38. Also, with English translation, in Gödel 1986, pp. 286–295.
  • Gödel, K., 1933f, “Eine Interpretation des intuitionistischen Aussagenkalküls”, Ergebnisse eines mathematischen Kolloquiums, 4: 39–40. Also, with English translation, in Gödel 1986, pp. 300–303.
  • Gödel, K., 1958, “Über eine bisher noch nicht benutzte Erweiterung des finiten Standpunktes”, Dialectica, 12: 280–287. Also, with English translation, in Gödel 1990, pp. 240–251.
  • Gödel, K., 1970, “On an extension of finitary mathematics which has not yet been used”, Circulated earlier version of Gödel 1972.
  • Gödel, K., 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, pp. 271–280.
  • Gödel, K., 1986, Collected Works. I: Publications 1929–1936, eds. S. Feferman et al., Oxford: Oxford University Press.
  • Gödel, K., 1990, Collected Works. II: Publications 1938–1974, eds. S. Feferman et al., Oxford: Oxford University Press.
  • Gödel, K., 1995, Collected Works. III: Unpublished Essays and Lectures, eds. S. Feferman et al., Oxford: Oxford University Press.
  • Gödel, K., 2003a, Collected Works. IV: Correspondence A-G, eds. S. Feferman et al., Oxford: Oxford University Press.
  • Gödel, K., 2003b, Collected Works. V: Correspondence H-Z, eds. S. Feferman et al., Oxford: Oxford University Press.
  • van Heijenoort, J. (ed.), 1967, From Frege to Gödel: A Sourcebook in Mathematical Logic, 1879–1931, Cambridge MA: Harvard University Press.
  • Herbrand, J., 1931, “Sur la non-contradiction de l’arithmétique”, Journal für die reine und angewandte Mathematik, 166: 1–8. Also Herbrand 1968, pp. 221–232. English translation in van Heijenoort 1967, pp. 620–628, reprint in Herbrand 1971, pp. 284–297.
  • Herbrand, J., 1968, Écrits logiques (ed. J. van Heijenoort), Paris: Presses Unversitaires de France.
  • Herbrand, J., 1971, Logical Writings (ed. W. Goldfarb), Cambridge, MA: Harvard University Press.
  • Hesseling, D., 2003, Gnomes in the Fog. The Reception of Brouwer's Intuitionism in the 1920s, Basel: Birkhäuser.
  • Heyting, A., 1925, Intuïtionistische axiomatiek der projektieve meetkunde, Ph.D. thesis, Universiteit van Amsterdam.
  • Heyting, A., 1928, [Prize essay on the formalization of intuitionistic logic]. Expanded and revised version published as Heyting 1930, Heyting 1930A, Heyting 1930B.
  • Heyting, A., 1930, “Die formalen Regeln der intuitionistischen Logik I”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 42–56. English translation in Mancosu 1998, pp. 311–327.
  • Heyting, A., 1930A, “Die formalen Regeln der intuitionistischen Logik II”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 57–71.
  • Heyting, A., 1930B, “Die formalen Regeln der intuitionistischen Logik III”, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 158–169.
  • Heyting, A., 1930C, “Sur la logique intuitionniste”, Académie Royale de Belgique, Bulletin de la Classe des Sciences, 16: 957–963. English translation in Mancosu 1998, pp. 306–310.
  • Heyting, A., 1931, “Die intuitionistische Grundlegung der Mathematik”, Erkenntnis, 2: 106–115. English translation in Benacerraf and Putnam 1983, pp. 52–61.
  • Heyting, A., 1932, “A propos d’un article de MM. Barzin et Errera”, Enseignement Mathématique, 31: 121–122.
  • Heyting, A., 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.
  • Heyting, A., 1934, Mathematische Grundlagenforschung, Intuitionismus, Beweistheorie, Berlin: Springer.
  • Heyting, A., 1956, Intuitionism, an Introduction, Amsterdam: North–Holland.
  • Heyting, A., 1958A, “Blick von der intuitionistischen Warte”, Dialectica, 12: 332–345.
  • Heyting, A., 1958C, “Intuitionism in mathematics”, in La philosophie au milieu du vingtiè me siè cle, R. Klibansky, ed., Firenze: La nuova Italia, vol. 1, 101–115.
  • Heyting, A., 1968A, “L.E.J. Brouwer”, in Contemporary Philosophy. A Survey. Vol.1: Logic and Foundations of Mathematics., R. Klibansky, ed., La Nuova Italia editrice, 308–315.
  • Heyting, A., 1974, “Intuitionistic views on the nature of mathematics”, Synthese, 27: 79–91.
  • Heyting, A., 1978, “History of the foundations of mathematics”, Nieuw Archief voor Wiskunde, XXVI(3): 1–21.
  • Hilbert, D., 1900, “Mathematische Probleme. Vortrag, gehalten auf dem internationalen Mathematiker-Kongress zu Paris 1900”, Archiv der Mathematik und Physik (3), 1: 44–63,213–237. English translation in the Bulletin of the American Mathematical Society 8:437 – 479, 1902.
  • Hilbert, D., 1922, “Neubegründung der Mathematik (Erste Mitteilung)”, Abhandlungen aus dem Mathematischen Seminar der Hamburgischen Universität, 1: 157–177. English translation in Mancosu 1998, pp. 198–214.
  • Hilbert, D., 1923, “Die logischen Grundlagen der Mathematik”, Mathematische Annalen, 88: 151–165. English translation in Ewald 1996, pp. 1134–1148.
  • Hilbert, D. and Ackermann, W., 1928, Grundzüge der theoretischen Logik, Berlin: Springer.
  • Joosten, J., 2004, Interpretability formalized, Ph.D. thesis, Utrecht University. Quaestiones Infinitae vol. XLIX, [Available from Universiteit Utrecht/Universiteitsbibliotheek].
  • Kennedy, J., 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, S., 1945, “On the interpretation of intuitionistic number theory”, Journal of Symbolic Logic, 50: 109–124.
  • Kleene, S., 1952, Introduction to Metamathematics, Amsterdam: North-Holland.
  • Kleene, S., 1973, “Realisability: a retrospective survey”, in Cambridge Summer School in Mathematical Logic 1971, H. Rodgers and A. Mathias, eds., Heidelberg: Springer, vol. 337 of Lecture Notes in Mathematics, 95–112.
  • Kleene, S. and Vesley, R., 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, Amsterdam: North-Holland.
  • Kolmogorov, A., 1925, “O principe tertium non datur”, Matematiceskij Sbornik, 32: 646–667. English translation in van Heijenoort 1967, pp. 416–437.
  • Kolmogorov, A., 1932, “Zur Deutung der intuitionistischen Logik”, Mathematische Zeitschrift, 35: 58–65. English translation in Mancosu 1998, pp. 328–334.
  • Kolmogorov, A., 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 original available online].
  • Kreisel, G., 1962, “Foundations of intuitionistic logic”, in Logic, Methodology and Philosophy of Science, Proc. 1960 Int. Congr., E. Nagel, P. Suppes, and A. Tarski, eds., Stanford: Stanford University Press, 198–210.
  • Kreisel, G., 1987, “Gödel's excursions into intuitionistic logic”, in Gödel remembered, P. Weingartner and L. Schmetterer, eds., Napoli: Bibliopolis, 67–179.
  • Kripke, S., 1965, “Semantical analysis of intuitionistic logic I”, in Formal Systems and Recursive Functions, M. Dummett and J. Crossley, eds., Amsterdam: North-Holland, 92–130.
  • Kuiper, J., 2004, Ideas and Explorations. Brouwer's Road to Intuitionism, Ph.D. thesis, Utrecht University. Quaestiones Infinitae vol. XLVI [Available from Universiteit Utrecht/Universiteitsbibliotheek].
  • Mancosu, P., 1998, From Brouwer to Hilbert. The Debate on the Foundations of Mathematics in the 1920s, Oxford: Oxford University Press.
  • McKinsey, J., 1939, “Proof of the independence of the primitive symbols of Heyting's calculus of propositions”, Journal of Symbolic Logic, 4(4): 155–158.
  • Mints, G., 2006, “Notes on constructive negation”, Synthese, 148: 701–717.
  • Moschovakis, J., 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, J., 1968, “Notes towards an axiomatization of intuitionistic analysis”, Logique et Analyse, 35: 280–297.
  • Parsons, C., 1967, [Introduction to the translation of sections 1–3 of Brouwer 1927B], in van Heijenoort 1967, pp. 446–457.
  • Pieri, M., 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.
  • Posy, C., 1992, “Review: Dirk van Dalen, Intuitionistic Logic; Walter Felscher, Dialogues as a Foundation for Intuitionistic Logic”, Journal of Symbolic Logic, 57(2): 754–756.
  • Russell, B., 1903, The Principles of Mathematics, London: Allen & Unwin.
  • Sato, M., 1997, “Classical Brouwer-Heyting-Kolmogorov interpretation”, RIMS Kokyuroku, 1021: 28–47.
  • Smirnov, V. 1925 [published 1932], “Kolmogorov, A.N.: Über das Prinzip tertium non datur.” Jahrbuch über die Fortschritte der Mathematik 51.0048.01 [Listing in ERAM database].
  • van Stigt, W., 1990, Brouwer's Intuitionism, Amsterdam: North-Holland.
  • Stone, M., 1937, “Topological representations of distributive lattices and Brouwerian logics”, Časopis pro pěstování matematiky a fysiky, 67: 1–25.
  • Sundholm, G., 1983, “Constructions, proofs and the meaning of logical constants”, Journal of Philosophical Logic, 12: 151–172.
  • Sundholm, G., 2004, “The proof-explanation of logical constants is logically neutral”, Revue Internationale de Philosophie, 58(4): 401–410.
  • Sundholm, G. and van Atten, M., 2008, “The proper explanation of intuitionistic logic: on Brouwer's proof of the Bar Theorem”, in van Atten et al. 2008, 60–77.
  • de Swart, H., 1976, “Another intuitionistic completeness proof”, Journal of Symbolic Logic, 41(3): 644–662.
  • de Swart, H., 1977, “An intuitionistically plausible interpretation of intuitionistic logic”, Journal of Symbolic Logic, 42(4): 564–578.
  • Tarski, A, 1938, “Der Aussagenkalkül und die Topologie”, Fundamentae Mathematicae, 31: 103–134. English translation in Tarski 1956, pp. 421–454.
  • Tarski, A., 1953, “A general method in proofs of undecidability”, in Undecidable theories, A. Tarski, A. Mostowski, and R. Robinson, eds., North- Holland, 3–35.
  • Tarski, A, 1956, Logic, Semantics, Metamathematics. Papers from 1923 to 1938, trl. J. Woodger, Clarendon Press.
  • Troelstra, A., 1977, “Aspects of constructive mathematics”, in Handbook of Mathematical Logic, J. Barwise, ed., Amsterdam: North-Holland, 973–1052.
  • Troelstra, A., 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.
  • Troelstra, A., 1990, “On the early history of intuitionistic logic”, in Mathematical Logic, P. Petkov, ed., New York: Plenum Press, 3–17.
  • Troelstra, A., Niekus, J., and van Riemsdijk, H., 1981, “Bibliography of A. Heyting”, Nieuw Archief voor Wiskunde, 29: 24–35.
  • Troelstra, A. and van Dalen, D., 1988, Constructivism in Mathematics, 2 vols., Amsterdam: North-Holland.
  • Veldman, W., 1976, “An intuitionistic completeness theorem for intuitionistic predicate logic”, Journal of Symbolic Logic, 41(1): 159–166.
  • Veldman, W., 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.
  • Vesley, R., 1980, “Intuitionistic Analysis: the Search for Axiomatization and Understanding”, in The Kleene Symposium, J. Barwise, H. J. Keisler, and K. Kunen, eds., Amsterdam: North-Holland, 317–331.
  • Wajsberg, M., 1938, “Untersuchungen über den Aussagenkalkül von A. Heyting”, Wiadomosci Matematyczne, 46: 45–101.
  • Wang, H., 1987, Reflections on Kurt Gödel, Cambridge MA: MIT Press.
  • Wavre, R., 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: 435–470.
  • Wavre, R., 1926, “Logique formelle et logique empirique”, Revue de Métaphysique et de Morale, 33: 65–75.
  • Weyl, H., 1921, “Über die neue Grundlagenkrise der Mathematik”, Mathematische Zeitschrift, 10: 39–79. English translation in Mancosu 1998, pp. 86–118.
  • Whitehead, A., 1906, The Axioms of Projective Geometry, Cambridge University Press.
  • Whitehead, A. and Russell, B., 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 and clarifications. Dirk van Dalen kindly granted permission to quote from materials in the Brouwer Archive. Thanks also to Dirk van Dalen and Eckhart Menzler-Trott for their search for Bernays' letter to Brouwer. In section 3.6 I have drawn on van Atten 2004a; I thank the Association for Symbolic Logic for granting permission to do this.

Copyright © 2009 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]