# 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
- 2 Brouwer's views on logic in 1907 and 1908
- 3 Brouwer's later refinements and applications, 1921–1955
- 3.1 The implicit Proof Interpretation
- 3.2 Widening the scope of the weak counterexamples
- 3.3 Strong counterexamples and the Creating Subject
- 3.4 The classification of propositions
- 3.5 Brouwer's view on the formalist program and Gödel's incompleteness theorems
- 3.6 Brouwer's logic and the Grundlagenstreit

- 4 Early partial formalizations and metamathematics
- 5 The Proof Interpretation made explicit
- Bibliography
- Other Internet Resources
- Related Entries

## 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∧Bis given by presenting a proof ofAand a proof ofB.(H2) A proof of A∨Bis given by presenting either a proof ofAor a proof ofB(plus the stipulation that we want to regard the proof presented as evidence forA∨B).(H3) A proof of A→Bis a construction which permits us to transform any proof ofAinto a proof ofB.(H4) Absurdity ⊥ (contradiction) has no proof; a proof of ¬ Ais a construction which transforms any hypothetical proof ofAinto a proof of a contradiction.(H5) A proof of ∀ xA(x) is a construction which transforms a proof ofd∈D(Dthe intended range of the variablex) into a proof ofA(d).(H6) A proof of ∃ xA(x) is given by providingd∈D, and a proof ofA(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*(*P**x* ∨
¬ *P**x*), 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 Ais given by presenting a mathematical construction in Brouwer's sense that makesAtrue.

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]}

IfU⊢AthenV⊢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 toassumeto 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 forAare 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 ofAwhich respects the specifications. Once this is accomplished, we can turn to the “implication” construction forB, which yields the construction forBand to the required embedding of the structure forAinto the structure forB. (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 establishA→B, one has to conceive ofAandBas conditions on constructions, and to show that from the conditions specified byAone obtains the conditions specified byB, 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 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 sensea, and from that deduce a contradiction. But then it would have been proved that not-ais 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):

- The relations
*r*=*s*,*r*<*s*and*r*>*s*are mutually exclusive. - From
*r*=*u*,*s*=*v*and*r*<*s*follows*u*<*v*. - From the simultaneous failure of the relations
*r*>*s*and*r*=*s*follows*r*<*s*. - From the simultaneous failure of the relations
*r*>*s*and*r*<*s*follows*r*=*s*. - 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 ∃*x*
*P*(*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:

- The continuum is totally ordered (Brouwer 1924N)
- Every set is either finite or infinite (Brouwer 1924N)
- The Heine-Borel theorem (Brouwer 1924N)
- ∀
*x*∈**R**(*x*∈**Q**∨*x*∉**Q**) (Brouwer 1925E) - Any two straight lines in the Euclidian plane are either parallel, or coincide, or intersect (Brouwer 1929A)
- 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:

- α has been proved to be true;
- α has been proved to be false, i.e. absurd;
- α 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;
- α 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 thewholemathematics, and no decision procedure for the whole mathematics. In each and everyclosed languagethere are only countably many expressions. Thecontinuumappears only in “the whole of mathematics” … If we haveonly 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:

*A*→ (*B*→*A*)- (
*A*→ (*A*→*B*)) → (*A*→*B*) - (
*A*→ (*B*→*C*)) → (*B*→ (*A*→*C*)) - (
*B*→*C*) → ((*A*→*B*) → (*A*→*C*)) - (
*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^{*}= ¬¬ Afor atomicAF(φ_{1}, φ_{2},… ,φ_{k})^{*}= ¬¬ F(φ_{1}^{*}, φ_{2}^{*}, … ,φ_{k}^{*}) for composed formulas

and proves this interpretability result:

IfU⊢_{H}φ thenU^{*}⊢_{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

- construct such a system and to indicate its deviations from Brouwer's theories;
- to investigate whether from the system to be constructed a dual system may be obtained by (formally) interchanging the
principium tertii exclusiand theprincipium 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:

*p*→*p*- (
*p*→*q*) → ((*q*→*r*) → (*p*→*r*)) - (
*p*∧*q*) →*p* - (
*p*∧*q*) →*q* - (
*r*→*p*) → ((*r*→*q*) → (*r*→ (*p*∧*q*))) *p*→ (*p*∨*q*)*q*→ (*p*∨*q*)- (
*p*→*r*) → ((*q*→*r*) → ((*p*∨*q*) →*r*)) - (
*p*→*q*) → ((*p*→ ¬*q*) → ¬*p*)

From these axioms, he then proved

- ¬¬(
*p*∨ ¬*p*) - ¬¬¬
*p*→ ¬p - ((¬
*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:

- If
*p*is provable in classical propositional logic, then ¬¬*p*is provable in intuitionistic propositional logic; - 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:

- (
*p*→ (*q*→*r*)) → (*q*→ (*p*→*r*)) - (
*p*→ (*p*→*r*)) → (*p*→*r*) *p*→ (*q*→*p*)- ¬
*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:

*a*→ (*a*∧*a*)- (
*a*∧*b*) → (*b*∧*a*) - (
*a*→*b*) → ((*a*∧*c*)→ (*b*∧*c*)) - ((
*a*→*b*) ∧ (*b*→*c*)) → (*a*→*c*) -
*b*→ (*a*→*b*) - (
*a*∧ (*a*→*b*)) →*b* *a*→ (*a*∨*b*)- (
*a*∨*b*) → (*b*∨*a*) - ((
*a*→*c*) ∧ (*b*→*c*)) → ((*a*∨*b*) →*c*) - ¬
*a*→ (*a*→*b*) - ((
*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 axiomsand theoremsof 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 capturedalladmissible 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 formulaa→bgenerally means: “Ifais correct, thenbis correct too.” This proposition is meaningful ifaandbare constant propositions about whose correctness nothing need be known … The case if conceivable that after the statementa→bhas been proved in the sense specified, it turns out thatbis always correct. One accepted, the formulaa→bthen has to remain correct; that is, we must attribute a meaning to the sign → such thata→bstill holds. The same can be remarked in the case where it later turns out thatais 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):

- to explicate and develop the meaning explanation that had given rise to Heyting's system;
- to engage in metamathematical study of the formal systems distilled from Heyting's system;
- 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

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

- 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 thatIf

**IPC**⊢*A*then**S4**⊢*A*′For more details on this result, see the section

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).*Gödel's Work in Intuitionistic Logic and Arithmetic*of Kennedy 2007, as well as Artemov 2001.^{[30]} - 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*

- the Disjunction Property (DP): if
⊢
- 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 theBrouwerian assertionofp: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:

⊢¬pwill mean: “It is known how to reducepto 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 byp′, but it must be realized thatp′ will hardly ever be a definitive statement, since it is necessary to take into account the possibility that the proof of eitherpor ¬pmight one day succeed. If one does not wish to risk having to retract what one has said, in the casep′ 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 constantCis rational”, expresses the expectation that we could find two integersaandbsuch thatC=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 betweenpand +pvanishes as soon a construction is intended inpitself, 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 “pis 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 intentionspandqis 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 “Cis not rational”, therefore, signifies the expectation that one can derive a contradiction from the assumption [Annahme] thatCis 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 ofa→bby “When I thinka, I must thinkb” 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: “Whenahas been proved, so hasb”, is not wholly satisfactory to me; when I ask myself what you may mean by that, I believe that alsoa→b, like the negation, should refer to a proof procedure: “I possess a construction that derives from every proof ofaa proof ofb”. In the following, I will keep to this interpretation. There is therefore no difference betweena→band +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:

Ifaandbare two problems, thena∧bdesignates the problem “to solve both problemsaandb”, whilea∨bdesignates the problem “to solve at least one of the problemsaandb”. Furthermore,a⊃bis the problem “to solvebprovided that the solution forais given” or, equivalently, “to reduce the solution ofbto the solution ofa” … ¬adesignates the problem “to obtain a contradiction provided that the solution ofais given” … (x)a(x) stands in general for the problem “to give a general method for the solution ofa(x) for every single value ofx”. (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 problema, either to find a solution fora, or to infer a contradiction from the existence of a solution fora!In particular, if the problem

aconsists 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 ofErkenntnis2, 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:

- propositions express intentions towards constructions
- 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 solvingaat the same time reduces the solution of any problem whatsoever to that ofa. (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):

- “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.” - “
*p*∧*q*can be asserted if and only if both*p*and*q*can be asserted.” - “
*p*∨*q*can be asserted if and only if at least one of the propositions*p*and*q*can be asserted. - “¬
*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.” - “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*.” - “⊢
(∀
*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*).” - “(∃
*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 thatp→qcan be asserted if and only if we possess a construction which, joined to the constructionp, would proveq. Now suppose that ⊢ ¬p, that is, we have deduced a contradiction from the supposition thatpwere carried out. Then, in a sense, this can be considered as a construction, which, joined to a proof ofp(which cannot exist) leads to a proof ofq. (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 = <http://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 = <http://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.

## Other internet resources

- Review of Hesseling's
*Gnomes in the Fog*in the*Bulletin of Symbolic Logic*(Postscript). - Dirk van Dalen's Brouwer bibliography,
updated version in van Atten
*et al*. 2008, pp. 343–390.

[Please contact the author with further suggestions.]

## Related Entries

Brouwer, Luitzen Egbertus Jan |
Gödel, Kurt |
Hilbert, David |
Hilbert, David: program in the foundations of mathematics |
logic: classical |
logic: intuitionistic |
logic: provability |
logic: relevance |
mathematics, philosophy of: formalism |
mathematics, philosophy of: intuitionism |
mathematics: constructive |
*Principia Mathematica* |
proof theory |
proof theory: development of |
set theory: constructive and Intuitionistic ZF |
Wittgenstein, Ludwig: philosophy of mathematics

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