% plain TeX
\magnification=\magstep1
% FORMATTING
\font\ninerm=cmr9
\font\ninebf=cmbx9
\font\nineit=cmti9
\font\ninei=cmmi9
\font\eighti=cmmi8
\font\eightrm=cmr8
\font\eightbf=cmbx8
\font\eightit=cmti8
\font\eightsl=cmsl8
\font\eighttt=cmtt8
\font\tenss=cmss10
\font\ninesy=cmsy9
\font\eightsy=cmsy8
\font\nineit=cmti9
\font\eightit=cmti8
\font\sixrm=cmr6
\font\sixbf=cmbx6
\font\sixi=cmmi6
\font\sixsy=cmsy6
\font\sans=cmss10
\font\eightsans=cmss8
\font\sansit=cmssi10
\font\tenmsa=msam10
\font\bbbold=msbm10
\def\bbb#1{\hbox{\bbbold#1}}
\def\cali#1{\hbox{$\cal#1$}}
\def\ninepoint{\def\rm{\fam0\ninerm}%
\textfont0=\ninerm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
\textfont1=\ninei \scriptfont1=\sixi \scriptscriptfont1=\fivei
\textfont2=\ninesy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
\textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
\textfont\itfam=\nineit \def\it{\fam\itfam\nineit}%
\textfont\bffam=\ninebf \scriptfont\bffam=\sixbf
\scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\ninebf}%
\normalbaselineskip=11pt
\setbox\strutbox=\hbox{\vrule height8pt depth 3pt width0pt}%
\let\big=\ninebig \normalbaselines\rm}
% MACROS
\everymath{\rm}
\def\C{{\nineit C}}
\def\I{{\nineit I}}
% TEXT
\noindent{\it Gnomes in the Fog: The Reception of Brouwer's Intuitionism
in the 1920s}, by Dennis E.~Hesseling, Science Networks -- Historical
Studies, vol.~28, Birkh\"auser, Basel, 2003, xxviii+447 pp.,
ISBN 3-7643-6536-6\footnote{}{2000 {\it Mathematics Subject Classification}.
01A60, 03-03, 03F55, 03B20.}
\bigskip
A classical mathematician \C\ and an intuitionist \I\ use the same logical
operators, $\land\ \forall\ \to\ \neg\ \exists\ \vee$, but with different
semantics and different deductive procedures. When \C\ asserts a closed
formula $A$, she is making an ontological statement: $A$ is true in the
structure under consideration. Then $A \vee \neg A$ always holds: either
$A$ is true or it is not, there is no third possibility. But when \I\
asserts $A$, he is making an epistemological statement: I know $A$. Thus
to him, $A \vee \neg A$ means: I know $A$ or I know that $A$ is absurd---but
now there is clearly a third possibility. He rejects the principle of the
excluded middle because to him it is a principle of omniscience.
I overheard two conversations between \C\ and \I. She spoke first:
\medskip
{\narrower\narrower\ninepoint
I have just proved $\exists xA$.
Congratulations! What is it?
I don't know. I assumed $\forall x\neg A$ and derived a contradiction.
Oh. You proved $\neg\forall x\neg A$.
That's what I said.
}
\medskip
{\narrower\narrower\ninepoint
I have proved $A \vee B$.
Good. Which did you prove?
What?
You said you proved $A$ or $B$; which did you prove?
Neither; I assumed $\neg A \land \neg B$ and derived a contradiction.
Oh, you proved $\neg[\neg A \land \neg B]$.
That's right. It's another way of saying the same thing.
}
\medskip
\noindent He does not agree with her last statement, of course, but at
least \C\ can explain to him what she has proved in a way that he can
understand. This elimination of $\exists$ and $\vee$ must continue all
the way, in the component formulas $A$ and $B$, until atomic formulas are
reached. Here \C\ and \I\ agree if they are discussing arithmetic, but
in analysis \C\ must explain an atomic formula $C$ as meaning $\neg\neg\,C$
to \I.
Now that \C\ has explained her theorem, will \I\ accept her proof?
Yes, G\"odel showed this in a remarkable five page paper published
in 1933 [G\"o]. At least, this is so for arithmetic. In set theory, \I\ will
admit the correctness of the deduction but the axioms of set theory will
be gibberish to him.
The moral of G\"odel's result is that Brouwer did not require a
{\it restriction}\/ of classical mathematics, as both he and his opponents
believed, but rather provided an {\it extension}\/ of it: he introduced
two new logical operators, the constructive $\exists$ and the constructive
$\vee$ different from their classical counterparts. The intuitionistic
semantics and proof syntax for $\exists xA$ and $A \vee B$ are quite
different from those for $\neg \forall x \neg A$ and
$\neg[\neg A \land \neg B]$. Stricter standards of proof are required and
richer information is obtained.
To \C, a closed formula $C$ contains one bit of information: true or false.
To \I, $C$ is an incomplete communication. For example, if $C$ is
$\exists x A$ and \I\ asserts that he knows $C$, then he is saying that
he knows a number $n$ (let us stick to arithmetic) such that he knows
$A_x[n]$, and similarly for $A \vee B$ he asserts that he knows $A$ or
$B$ and is prepared to say which.
Kleene, not himself an intuitionist, saw deeply into the nature of
intuitionism and formalized intuitionistic knowledge in terms of
{\it realizability}. He encoded intuitionistic knowledge of $C$ in a code $c$,
far richer than the classical true or false; see [Kl45] and [Kl52,~\S82].
The intuitionistic knowledge of a closed formula $C$ of arithmetic can
be explained in terms of an interactive program:
\bigskip
{\ninepoint
\halign{\qquad\hfil#\hfil&\quad\hfil#\hfil&\quad#\hfill\cr
If $C$ is:&and the code $c$ is:&the program:\cr
&&\cr
atomic&anything&evaluates $C$ as true or false.\cr
$A\land B$&$\langle a,b\rangle$&splits into two child processes,
with code $a$ for $A$ and $b$ for $B$.\cr
$\forall xA$&$c$&prompts for a number input $n$ and
runs $c\{n\}$ on $A_x[n]$.\cr
$A\to B$&c&prompts for code input $a$ and forms a pipe: it runs $a$ on $A$,\cr
&&and if this terminates, runs $c\{a\}$ on $B$.\cr
$\exists xA$&$\langle n,a\rangle$&prints the output number $n$ and runs
$a$ on $A_x[n]$.\cr
$A\vee B$&$\langle 1,a\rangle$&prints ``first'' and runs $a$ on $A$.\cr
$A\vee B$&$\langle 2,a\rangle$&prints ``second'' and runs $a$ on $B$.\cr}
\bigskip
}
\noindent(We can replace $\neg A$ by $A\to0=1$, so $\neg$ does not require
separate discussion.)
Then ``$c$ realizes $C$'' means that $c$ is correct code for the interactive
program $C$. As the program runs, it also reduces the code to a form
suitable for the subformulas that are encountered.
A fuller account of Kleene's realizability in terms of programming is
available online [ENe].
The nature of intuitionism was greatly clarified by Heyting when he
formalized the intuitionistic predicate calculus and intuitionistic
arithmetic in 1930. (Full disclosure: the reviewer is a formalist.)
Kleene introduced realizability in the expectation that every theorem
of intuitionistic arithmetic S was realizable, and David Nelson established
this by an algorithm [DNe].
The high point of this beautiful result is his proof by a single
induction that every induction axiom is realizable. Since $0=1$ is not
realizable, Nelson's theorem entails a consistency proof for S and so
a fortiori for Peano Arithmetic P (since by the G\"odel interpretation
S is an extension of P). The realization predicate cannot itself be expressed
in arithmetic, so conflict with G\"odel's second theorem, on the impossibility
of self-consistency proofs, is avoided.
Call a formula {\it classical}\/ in case it does not contain the output
operators $\exists$ or
$\vee$. For a classical closed formula $C$ of arithmetic, ``$c$ realizes $C$''
does not depend on the code $c$ and, from a classical perspective, is
equivalent to the classical true-false notion. The extra constructive
information that a realization code $c$ contains is algorithms for
constructing existentially quantified objects and for deciding between
alternatives. This is why intuitionistic reasoning is important to
programming. Thanks to Kleene, the two constructive tendencies,
algorithms and intuitionism, met.
The connection between intuitionism and programming is deeply
pursued by Per Martin-L\"of and his school; see [M-L] and [NoPeSm].
Kleene's explanation of intuitionistic knowledge is semantic and does not
refer to proofs at all. But many intuitionists attempt to explain the
intuitionistic meaning of the input operators $\forall$, $\to$, and $\neg$
syntactically in terms of proofs, as in
``$A\to B$ means that I know how from a proof
of $A$ to find a proof of $B$''. This viewpoint has been vigorously
questioned by Dummett [Du]. Taken literally, it would mean that we could
dispense with modus ponens, which is the rule of inference: from $A$
and $A\to B$ infer $B$. But if $A\to B$ means that I know how from a
proof of $A$ to find a proof of $B$, why not just do it rather than bother
with $A\to B$? Alternatively, if one attempts to construct a syntactical
predicate ``$c$ verifies $C$'' along the lines of Kleene's semantic
predicate ``$c$ realizes $C$'', it runs afoul of G\"odel's second theorem
and $\neg\neg\,0=0$ turns out to be ``unverifiable''; see [ENe]. No one
has given an account of the usual intuitionistic description of the
meaning of $\to$ that manages, in Dummett's words, ``to escape, not
merely circularity, but total vacuousness''.
Curiously, the question of the intuitionistic meaning of $\to$ does not
seem to have played any role in the debate of the 1920s, though the meaning
of $\exists$ and $\vee$ was central.
And this brings us to the book under review, whose main focus is on the
debate from the appearance of Weyl's {\it Grundlagenkrise}\/ in 1921 to about
1928. It is a fascinating story. If you have a strong interest in
foundations, you will begin at the beginning, continue until you reach the
end, then stop. Those with a more peripheral interest in the subject
will enjoy reading the conclusions to each chapter and to the book,
browsing in the
author index to see the roles in the debate of
Kolmogorov, L\'evy, Zariski, and many more, and skimming here and there.
I found Chapter 1 on Brouwer's predecessors gripping and Chapter 6 on
the cultural context less so.
I have said nothing in this article about Brouwer's ``second act of
intuitionism'' (\S2.6) and free choice sequences, but it makes interesting
reading. There seems to be a consensus that Bishop's non-intuitionistic
constructive analysis [Bi] is preferable to Brouwer's approach to analysis.
The author, Dennis Hesseling, is a mathematician with an additional
background in history and
philosophy, and he speaks with confidence in all three areas. A book as
fine as this deserves more care from its publisher. In a number of places,
particularly in footnotes and the glossary, formulas are garbled, with
$\overline{\phantom A}$ printed instead of the intended symbol. The author's
English is fluent and a pleasure to read, but there is an occasional
unidiomatic usage which careful editing would have corrected.
In strong contrast to the other great scientific debate of the twentieth
century, that between Niels Bohr and Einstein, the debate between
Brouwer and Hilbert was acerbic, with uncollegial words and acts, primarily
on the part of Hilbert (see especially \S2.8). It strikes me as a curious
historical fact that Bohr persuaded physicists, who used to study the
real world, to give up their belief in the objective reality of the physical
world whereas
mathematicians, who study an abstract world that we ourselves create,
followed Hilbert (who was a Platonist at heart) in refusing to abandon
our belief in the objective reality of mathematical entities.
Hilbert's program to secure the foundations of mathematics by finitary
means is often called a failure. But it achieved several things of
fundamental value and lasting importance.
Before the Formalist Enlightenment, even mathematicians who like Peano
and Zermelo were striving to be formal did not make an absolute
distinction between syntax and semantics. The distinction is essential;
an axiom system in which one is required to understand the meaning of
some of the axioms is not an axiomatization at all. This distinction may
be due more to Hilbert's assistant Bernays than to Hilbert himself (\S5.2.2).
Thanks to this enlightenment, it became possible for the first time
to study theories with the same precision and clarity
with which one studies groups or fields.
Mathematics consists of reasoning and computation, and of the two
computation is the more fundamental. Aristotle, Leibniz, Boole,
and Hilbert each took a big step towards realizing the vision
of reducing reasoning to computation.
One of the most interesting themes of ``Gnomes in the Fog'' is the
strong influence that Brouwer had on Hilbert's program. As Hesseling
documents, Brouwer's opposition was not to formalism, which hardly
existed at the time he founded intuitionism, but to classical mathematics
regarded as contentual. (This is a useful word that I learned from the
book. It is the English equivalent of the German {\it inhaltlich}, and
the OED defines it as ``Belonging to, or dealing with, content'' with the
first citation from 1909.) Gradually, step by step and without acknowledging
his debt to Brouwer, Hilbert retreated from a contentual view of classical
mathematics and refined the formalist position to the point
where consistency was to
be established essentially by intuitionistic methods. As Fraenkel
summarized the debate (\S3.2.2), ``As I see it, Brouwer has reached the
biggest success for his point of view by winning as an advocate of his
starting position---Hilbert! \dots\ Hilbert indeed has taken over the
demand for constructivity and the rejection of a contentual ground for the
application of Aristotelian logic on infinite totalities.''
In evaluating the work of those like Brouwer who have made truly
fundamental contributions to human knowledge---Columbus and Freud also
come to mind---we are in the position that our world outlook has been
completely changed by their work and we cannot picture what it was like
beforehand. Before Brouwer, were mathematicians aware that the usual proofs of
the fundamental theorem of algebra are not constructive (\S4.3)?
Let us honor those with the courage foolishly to set sail into unknown
seas and the endurance to reach land, though the land discovered differ
from the land of the vision. What is the fog and who are the gnomes?
The answer is found in the quotations with which this beautiful book
begins and ends.
\bigskip
\centerline{References}
\medskip
[Bi] Errett Bishop, ``Foundations of Constructive Analysis'',
McGraw-Hill, New York, 1967.
\smallskip
[Du] Michael Dummett, ``The philosophical basis of
intuitionistic logic'', Proceedings of the Logic Colloquium, Bristol,
July 1973, ed. H. E. Rose and J. C. Shepherdson, pp. 5--40,
North-Holland, Amsterdam, 1975. Reprinted in Paul Benacerraf and
Hilary Putnam, eds., ``Philosophy of Mathematics: Selected readings'',
2nd ed., Cambridge University Press, Cambridge, 1983.
\smallskip
[G\"o] Kurt G\"odel, ``Zur intuitionistischen
Arithmetik und Zahlentheorie'', Ergebnisse eines mathematischen
Kolloquiums, Heft 4, pp. 34--38, 1933.
\smallskip
[Kl45] S. C. Kleene, ``On the interpretation of intuitionistic number
theory'', Jour. Symbolic Logic, vol. 10, pp. 109--124, 1945.
\smallskip
[Kl52] S. C. Kleene, ``Introduction to Metamathematics'',
North-Holland, Amsterdam, 1971. First published 1952.
\smallskip
[M-L] Per Martin-L\"of,
``Intuitionistic Type Theory'', Bibliopolis, Naples, 1984.
\smallskip
[DNe] David Nelson, ``Recursive functions and intuitionistic
number theory'', Trans. Amer. Math. Soc., vol. 61, pp. 307--368, 1947.
\smallskip
[ENe] Edward Nelson, ``Understanding Intuitionism'', presented at
Rencontre du Reseau Georges Reeb, March 24-28, 1997, \hfill\break
{\tt http://www.math.princeton.edu/$\scriptstyle\sim$nelson/papers/int.pdf}
\smallskip
[NoPeSm] Bengt Nordstr\"om, Kent Petersson, Jan M. Smith,
``Programming in Martin-L\"of's Type Theory: An
Introduction'', The International Series of Monographs on
Computer Science 7, Clarendon Press, Oxford, 1990.
\bigskip
\hfill Edward Nelson
\hfill Princeton University
\hfill {\it E-mail address}\/: {\tt nelson@math.princeton.edu}
\bye
\medskip
{\hfill Edward Nelson}
{\hfill Princeton University}
{\hfill {\it E-mail address}: {\tt nelson@math.princeton.edu}
\bye