## 1. Introduction


### 1.1 The Proof Interpretation



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


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



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



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


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



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


### 1.2 Interpretation, Explanation, and Names



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


 

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


For the moment, we note that the BHK-Interpretation or Proof
Interpretation is not an interpretation in this mathematical sense,
but is rather a meaning explanation; we will come back to such
interpretations and their difference from explanations in Section 2
of the supplementary document
 The Turn to Heyting's Formalized Logic and Arithmetic.



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



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



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


## 2. Brouwer's Views on Logic in 1907 and 1908


### 2.1 Mathematics, Language, and Logic



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



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



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



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



or, in Heyting's words,



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



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



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



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



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



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



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



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



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



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



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


### 2.2 The Hypothetical Judgement



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



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



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



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


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



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



An alternative reading is \(\beta\):


* \((\beta)\) In order to
establish \(A \rightarrow B\), one has to conceive of \(A\)
and \(B\) as conditions on
constructions, and to show that from the conditions specified by \(A\)
one obtains the conditions specified by \(B\),
according to transformations whose composition
preserves mathematical constructibility: if, by hypothesis, a
construction for \(A\) has been made, then we can make
a construction for \(B\) (van Atten 2009:
128).



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



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



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



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


### 2.3 Negation



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



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


### 2.4 Weak Counterexamples ("unreliability") and Excluded Middle



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



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



> 
> 
> Is there in the decimal expansion of \(\pi\) a digit which occurs more
> often than any other one?
> 
> 
> 
> Do there occur in the decimal expansion of \(\pi\) infinitely many
> pairs of equal consecutive digits? (Brouwer 1908C: 7 [van Atten &
> Sundholm 2017: 44])
> 
> 
> 



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



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



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



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



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



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


### 2.5 There Are No Absolutely Undecidable Propositions



Brouwer continues this last quotation as follows:



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



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



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



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



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



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


## 3. Brouwer's Later Refinements and Applications, 1921-1955


### 3.1 The Implicit Proof Interpretation



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


#### 3.1.1 An equivalence in propositional logic



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



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


#### 3.1.2 The proof of the bar theorem



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



Brouwer's proof of the bar theorem from 1924 (later versions of
the proof appeared in 1927 and in 1954) proves a statement of the form
"If \(A\) has been demonstrated, then \(B\)
is demonstrable" (Brouwer 1924D1, 1927B,
1954A). This would evidently not be an implication \(A \rightarrow B\)
if the latter were 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 also chose to understand implication in this
stronger sense, that is, in terms of *assertion conditions*;
see
 section 5.4
 below.)



A simple but relevant version of the bar theorem (for the universal
tree over the natural numbers, *T*) would be:



> 
> 
> If it has been demonstrated that every path through \(T\)
> intersects a given set of nodes \(B\),
> then it can be demonstrated that every path through \(T\)
> has a node in common with a set of nodes \(B'\)
> that can be
>  well-ordered.[9]
> 
> 
> 



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



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



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



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


#### 3.1.3 Ordering axioms



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


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



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



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



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


### 3.2 Widening the Scope of the Weak Counterexamples



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


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


### 3.3 Strong Counterexamples and the Creating Subject



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



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



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

 

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


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



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



Using creating subject methods, Brouwer showed, for instance,



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


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


### 3.4 The Classification of Propositions



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


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



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



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


### 3.5 Brouwer's View on the Formalist Program and Godel's Incompleteness Theorems



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



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



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



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



Godel'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
Godel's first theorem in print; on the other hand, he
clearly had the second theorem in mind when he wrote, in 1952,
that



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



Hao Wang reports:



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



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



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



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



Indeed, according to Carnap, it had been an argument of
Brouwer's that had stimulated Godel in finding the first
theorem. In a diary note for December 12, 1929, Carnap states that
Godel 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 Godel
had told him:



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



This record contains in particular elements from the second of
Brouwer's two lectures in Vienna, in which one finds the
argument that Godel 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, Schroder) 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 (with a different meaning) 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 (Godel 2003a: 279), and
more generally never read Brouwer's papers (van Dalen 2005:
 637).[15])
 In addition, Brouwer did not announce the existence of strong
counterexamples in a loud or polemical way; and when in 1954 he
finally did publish (in English) a paper with a polemical
title--"An example of contradictority in classical theory
of functions"--the Foundational Debate was, in the social
sense, long over. Intuitionistic logic and mathematics had been widely
accepted to the extent that they could be seen as the constructive
part of classical mathematics, while the typically intuitionistic
innovations were ignored. It is not surprising, then, that the
presentation of the strong counterexamples in the 1950s did not at all
lead to a reopening of the debate. For further discussion of this
matter, see Hesseling 2003 and van Atten 2004a.


## 4. Early Partial Formalizations and Metamathematics



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



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



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



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



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


### 4.1 Kolmogorov 1925



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



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



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



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


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

 

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


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



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

 

\[ \begin{align\*} A^\* & = \neg \neg A & \textrm{for atomic } A\\ F(\phi\_1, \phi\_2 ,\ldots ,\phi\_k)^\* & = \neg \neg F(\phi\_{1}^\*, \phi\_{2}^\*,\ldots ,\phi\_{k}^\*) & \textrm{ for composed formulas} \end{align\*} \]


and proves this interpretability result:

 

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


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



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



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



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



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



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



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


### 4.2 Heyting 1928



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



> 
> 
> By its very nature, Brouwer's set theory cannot be identified
> with the conclusions formally derivable in a certain pasigraphic
> system [i.e., universal notation system]. Nevertheless certain
> regularities may be observed in the language which Brouwer uses to
> give expression to his mathematical intuition; these regularities may
> be codified in a formal mathematical system. It is asked to
> 
> 
> 1. construct such a system and to indicate its deviations from
> Brouwer's theories;
> 2. to investigate whether from the system to be constructed a dual
> system may be obtained by (formally) interchanging the *principium
> tertii exclusi* and the *principium contradictionis*.
> (Troelstra 1990: 4)
> 
> 
> 



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



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



Heyting's essay covered propositional logic, predicate logic,
arithmetic, and Brouwerian set theory or analysis. One would think
that, to be able to achieve this, Heyting must have had quite precise
ideas on how to explain the logical connectives intuitionistically.
However, Heyting's correspondence with Freudenthal in 1930 shows
that before 1930, Heyting had not yet arrived at the explicit
requirement of a transformation procedure in the explanation of
implication (see the
 quotation
 in
 section 5.1
 below).



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



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



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



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



> 
> 
> And, with an eye on SS13, 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 Lukasiewicz talked
about it to Bernays at the Bologna conference in 1928, and Church
mentioned it in a letter to Errera in 1929 (Hesseling 2003: 274).


### 4.3 Glivenko 1928 and 1929



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



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


From these axioms, he then proved

 

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


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



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



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


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



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



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

 

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


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



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



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


### 4.4 Heyting 1930



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



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



> 
> 
> Intuitionistic mathematics is a mental activity
> ["*Denktatigkeit*"], 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-a-vis ordinary language; and these are properties that
> facilitate the penetration into the intuitionistic concepts and the
> use of these concepts in research. (Heyting 1930: 42 [Mancosu 1998:
> 311])
> 
> 
> 



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



> 
> 
> I regret that my name is known to-day mainly in connection with these
> papers [Heyting 1930, 1930A, 1930B], which were very imperfect and
> contained many mistakes. They were of little help in the struggle to
> which I devoted my life, namely a better understanding and
> appreciation of Brouwer's ideas. They diverted the attention
> from the underlying ideas to the formal system itself. (Heyting 1978:
> 15)
> 
> 
> 



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



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



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

 

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


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



> 
> 
> I sifted the axioms *and theorems* of Principia Mathematica
> and, on the basis of those that were found to be admissible, looked
> for a system of independent axioms. Given the relative completeness of
> Principia, this to my mind ensures the completeness of my system in
> the best possible way. Indeed, as a matter of principle, it is
> impossible to be certain that one has captured *all* admissible
> modes of inference in one formal system. (Heyting to Becker, September
> 23, 1933 (draft) [van Atten 2005: 129], original italics, translation
> mine)
> 
> 
> 



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



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



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



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



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



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



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



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


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



By and large, these three roads lead to very different areas, with
correspondingly divergent histories, of which no unified account can
be expected. (However, in the Dialectica Interpretation, as proposed
and understood by Godel [1958, 1970, 1972], they came close to
one another.) 
Following the main theme of the present account, our topic
will remain the intuitionistic meaning explanation of logic. But a
number of early highlights of the formal turn are presented in this
supplementary document:



> 
> The Turn to Heyting's Formalized Logic and Arithmetic
> 


## 5. The Proof Interpretation Made Explicit


### 5.1 Heyting 1930, 1931



Heyting told van Dalen that he had the notion of (intuitionistic)
construction in mind to guide him in devising his formalization of
intuitionistic logic and mathematics in 1927. In the published version
of his formalization, he did not elaborate much on the meaning of the
connectives; all he explained there about the general meaning of \(a
\rightarrow b\) was that "If \(a\) is correct,
then \(b\) is correct too" (Heyting 1930: 44
[Mancosu 1998: 313]). Correspondence between Heyting and Freudenthal
in 1930 shows that Heyting up till then did not have a more refined
explanation at hand; we will come back to this later in this
section.



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



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



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



And then of intuitionistic negation:



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



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



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



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



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



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



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



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



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



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



The explanation of disjunction in the Konigsberg lecture is:



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



And of negation:



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



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



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



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



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


### 5.2 Influences on Heyting



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


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



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


### 5.3 Kolmogorov 1932 and Heyting 1934



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



Kolmogorov's idea is this:



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



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



> 
> 
> to give a general method that allows, for every problem \(a\),
> either to find a solution for \(a\),
> or to infer a contradiction from the existence of a solution for \(a\)!
> 
> 
> 
> In particular, if the problem \(a\) consists in the
> proof of a proposition, then one must possess a general method either
> to prove or to reduce to a contradiction any proposition. (Kolmogorov
> 1932: 63 [Mancosu 1998: 332]).
> 
> 
> 



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



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



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



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



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


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



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



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



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



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



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



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



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



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



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



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


### 5.4 Heyting 1956



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


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



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



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



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



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



Even within the intuitionistic movement, not everyone agreed with
Heyting's explanation of logic. This is discussed in a supplementary
document:



> 
> Objections to the Proof Interpretation
>