\input hmmac.tex
\raggedright
\raggedbottom
\parskip=\smallskipamount
\phantom.
\vskip2truein
\centerline{\bigrm Hilbert's Mistake}
\bigskip
\bigskip
\centerline{\it Edward Nelson}
\medskip
\centerline{\it Department of Mathematics}
\medskip
\centerline{\it Princeton University}
\vfill\eject
\centerline{\bigrm Abstract}
\bigskip
Hilbert was at heart a Platonist.
(``No one shall expel us from the paradise
that Cantor has created for us.'') His formalism
was primarily a tactic in his battle against Brouwer's
intuitionism.
\bigskip
His mistake was to pose the problem of \hfil\break
{\it showing that}\/
mathematics, beginning with Peano Arithmetic, is
consistent, rather than to ask {\it whether}\/ it is
consistent.
\bigskip
In this talk I give reasons for taking seriously
the possibility that contemporary mathematics,
including Peano Arithmetic, may indeed be inconsistent.
\vfill\eject
\centerline{\bigrm Potential vs.~Completed Infinity}
\bigskip
Let us distinguish between the \ii genetic., in the dictionary
sense of pertaining to
origins, and the \ii formal.. Numerals (terms containing only the unary function
symbol~S and the constant~0)
are genetic; they are formed by human activity.
All of mathematical activity is genetic, though the subject matter is formal.
\bigskip
Numerals constitute a \ii potential infinity.. Given any numeral, we can construct a new
numeral by prefixing it with~S.
\bigskip
Now imagine this potential infinity to be completed.
Imagine the inexhaustible process of constructing numerals somehow to have been finished,
and call the result \ii the set of all numbers., denoted by \N.
\bigskip
Thus $\N$ is thought to be an \ii actual infinity.\/ or a
\ii completed infinity.. This is curious terminology,
since the etymology of ``infinite'' is ``not finished''.
\vfill\eject
\noindent{\bf We were warned.}
\medskip
Aristotle: Infinity is always potential, never actual.
Gauss: I protest against the use of infinite magnitude as
something completed, which is never permissible in mathematics.
\bigskip
\noindent{\bf We ignored the warnings.}
\medskip
With the work of Dedekind, Peano, and Cantor above all,
completed infinity was accepted into mainstream mathematics.
Mathematics became a faith-based initiative.
\bigskip
\noindent{\bf Try to imagine \N\ as if it were real.}
A friend of mine came across the following on the Web:
\vfill\eject
\noindent{\eighttt www.completedinfinity.com}
\bigskip
\bigskip
\bigskip
\centerline{\bf \rgbo{1 0 0}{Buy a copy of \N\hskip.2pt!}}
\bigskip
{\bf
\noindent\rgbo{0 .7 0}{Contains zero---contains the successor
of everything it contains---contains only these.}
\medskip
Just \$100.
\bigskip
\noindent\rgbo{0 0 1}{Do the math! What is the price per number?}
\bigskip
{\it Satisfaction guaranteed!}
\bigskip
{\baselineskip=7pt
{\eightrm Use our secure form to enter your credit card number and its
security number, zip code, social security
number, bank's routing number, checking account number, date of birth, and
mother's maiden name.}
}
\bigskip
The product will be shipped to you within two business days in a plain wrapper.
}
\vfill\eject
My friend answered this ad and
proudly showed his copy of \N\ to me. I noticed that zero was green,
and that the successor of every green number
was green, but that his model contained a red number. I
told my friend that he had been cheated,
and had bought a nonstandard model, but he is color blind
and could not see my point.
\bigskip
I bought a
model from another dealer and am quite pleased with it. My
friend maintains that it contains an
ineffable number, although zero is effable and the successor of every
effable number is effable,
but I don't know what he is talking about. I think he is just jealous.
\bigskip
The point of this conceit is that it is impossible
to characterize~\N\ unambiguously, as we shall argue in detail.
\vfill\eject
As a genetic concept, the notion of numeral is clear.
The attempt to formalize the concept usually proceeds as follows:
\bigskip
\noj\llap{(i)}~zero is a number;
\noj\llap{(ii)}~the successor of a number is a number;
\noj\llap{(iii)}~zero is not the successor of any number;
\noj\llap{(iv)}~different numbers have different successors;
\noj\llap{(v)}~something is a number
only if it is so by virtue of (i) and~(ii).
\bigskip
We shall refer to this as the \ii usual definition..
Sometimes (iii) and~(iv) are not stated explicitly, but
it is the extremal clause~(v) that is unclear.
What is the meaning of ``by virtue of''?
It is obviously circular to define a number as something constructible by
applying (i) and~(ii) any number of times.
We cannot characterize numbers from
below, so we attempt to characterize them from above.
\vfill\eject
The study of the foundations of arithmetic began in earnest with the work of
Dedekind and Peano.
Both of these authors gave what today would be called set-theoretic
foundations for arithmetic.
In \ZFC\ (and extensions by definitions thereof) let us write
0 for the empty set and define the successor by
\noj $\'S'x=x\cup\{x\,\}$
\noin We define
\noj $x \' is inductive' \iff 0\in x \and \forall y[y\in x \imp \'S'y\in x]$.
\noin Then the axiom of infinity of \ZFC\ is
\noj $\exists x[x \' is inductive']$
\noin and one easily proves in \ZFC\ that there exists a
unique smallest inductive set; i.e.,
\noj $\exists!x\[x \' is inductive' \and \forall y[y \' is inductive'
\impP x\subseteq y]\]$
\vfill\eject
We define the constant~$\N$ to be this smallest
inductive set:
\noj $\N=x \iff x \' is inductive' \and
\forall y[y \' is inductive' \impP x\subseteq y]$
\noin and we define
\noj $x \' is a number' \iff x \in \N$.
\bigskip
Then the following are theorems:
\nok// 1. $0 \' is a number'$
\nok// 2. $x \' is a number' \imp \'S'x \' is a number'$
\nok// 3. $x \' is a number' \imp \'S'x\ne0$
\nok// 4. $x \' is a number' \and y \' is a number' \and x\ne y \imp
\'S'x\ne\'S'y$.
\vfill\eject
These theorems are a direct expression of \hfil\break
(i)--(iv) of the usual definition.
But can we express the extremal clause~(v)? The induction theorem
\noj $x \' is a number' \and y \' is inductive' \imp x \in y$
\noin merely asserts that for any property that can be expressed in \ZFC, if
0~has the property, and if the successor of every element that has the property also
has the property, then every number has the property.
\bigskip
We cannot say, ``For all numbers~$x$
there exists a numeral~d such that $x=\ro d$'' since this is a category mistake
conflating the formal with the genetic.
\vfill\eject
Using all the power of modern mathematics, let us try to formalize the concept
of number.
Let T be any theory whose language contains the constant 0, the unary function
symbol~S, and the unary predicate symbol ``is a number'', such that $(/ 1)$--$(/ 4)$
are theorems of~T.
For example, T~could be the extension by definitions of \ZFC\
described above or it could be Peano Arithmetic \PA\ with the definition: \hfil\break
$x \' is a number' \iffF x=x$.
\bigskip
Have we captured the intended meaning of the extremal clause (v)?
To study this question,
construct $\ro T^\phi$ by adjoining a new unary predicate symbol $\phi$ and the
axioms
\nok// 5. $\phi(0)$
\nok// 6. $\phi(x) \imp \phi(\'S'x)$.
\vfill\eject
Notice that $\phi$ is an undefined symbol.
If T is \ZFC, we cannot form
the set \hfil\break
$\{x\in\N\colon\phi(x)\,\}$ because the subset axioms of \ZFC\ refer only to
formulas of \ZFC\ and $\phi(x)$ is not such a formula. Sets are not genetic objects,
and to ask whether a set with a certain property exists is to ask whether a certain
formula beginning with~$\exists$ can be proved in the theory.
Similarly, if T is \PA\ we cannot apply induction to $\phi(x)$ since this
is not a formula of \PA. Induction is not a truth; it is an axiom scheme of a formal
theory.
If T is consistent then so is $\ro T^\phi$, because we can interpret
$\phi(x)$ by $x=x$. (And conversely, of course, if T~is inconsistent then
so is~$\ro T^\phi$.)
For any numeral S\dots S0 we can prove $\rm\phi(S\ldots S0)$ in S\dots S0 steps
using these two axioms and detachment (modus ponens).
\vfill\eject
Let d be a variable-free term.
{\bf Proving~$\rm\phi(d)$ in~$\ro T^\phi$ perfectly expresses the extremal clause,
that $\rm d$~is
a number by virtue of (i) and~(ii) of the usual definition. We can read $\phi(x)$ as
``$x$~is a number by virtue of (i) and~(ii)''.}
\bigskip
Therefore we ask: can
\nok// 7. $x \' is a number' \imp \phi(x)$
\noin be proved in $\ro T^\phi$?
That is, can we prove that our formalization
``$x$~is a number'' captures the intended meaning of the extremal clause?
Trivially yes if T is inconsistent, so assume
that T~is consistent.
Then the answer is no. Here is a semantic argument for
this assertion.
\vfill\eject
By $(/ 1)$--$(/ 4)$, none of the formulas
\noj $x \' is a number' \imp x=0 \,\orR\, x=\'S'0 \,\orR\,\cdots\,\orR\,
x=\'S'\ldots\'S'0$
\noin is a theorem of T. Hence the theory $\ro T_1$ obtained
from~T by adjoining a new constant~e and the axioms
\noj $\ro e \' is a number'$, $\ro e\ne0$, $\ro e\ne\'S'0$, \dots,
$\rm e\ne S\ldots S0$, \dots
\noin is consistent.
By the G\"odel completeness
theorem,
$\ro T_1$~has a model $\cal A$. Let $\cal X$ be the
smallest subset of the universe~$|\cal A|$
of the model containing $0_{\cal A}$ and closed under
the function $\ro S_{\cal A}$. Then $\ro e_{\cal A}$ is not
in~$\cal X$. Expand $\cal A$ to be a model ${\cal A}\phi$ of~$\ro T^\phi$ by
letting~$\phi_{{\cal A}\phi}$ be~$\cal X$. Then $(/ 7)$ is not valid in this model,
and so is not a theorem of~$\ro T^\phi$.
The conclusion to be drawn from this argument is that it is impossible to formalize
the notion of number in such a way that the extremal clause holds.
\vfill\eject
Despite all the accumulated evidence to the contrary,
mathematicians persist in believing in~$\N$ as a real object
existing independently of any formal human construction.
\bigskip
In a way this is not
surprising. Mathematics as a deductive discipline was
invented by Pythagoras, possibly with some influence from Thales.
The Pythagorean religion held that all is number, that the numbers
are pre-existing and independent of human thought. Plato was strongly influenced
by Pythagoras and has been called the greatest of the Pythagoreans.
\bigskip
Over two and a half millennia after Pythagoras,
most mathematicians continue to hold a religious belief in~$\N$
as an object existing independently of formal human construction.
\vfill\eject
\centerline{\bigrm Against Finitism}
\bigskip
There is obviously something inelegant about making arithmetic depend
on set theory. What today is called \ii Peano Arithmetic.\/ (\PA) is the
theory whose nonlogical symbols are the constant~0, the unary function symbol~S,
and the binary function symbols~$+$ and~$\.$, and
whose nonlogical axioms are
\nok// 8.\phantom0 $\'S'x\ne0$
\nok// 9.\phantom0 $\'S'x=\'S'y\imp x=y$
\nok// 10. $x+0=x$
\nok// 11. $x+\'S'y=\'S'(x+y)$
\nok// 12. $x\.0=0$
\nok// 13. $x\.\'S'y=(x\.y)+x$
\noin and all \ii induction formulas.
\nok// 14. $\rm A_x(0) \and \forall x[A \impP A_x(\'S'\ro x)] \imp \ro A$
\noin where A is any formula in the language of \PA.
\vfill\eject
How is the induction axiom scheme \nn/ 14. justified?
\bigskip
Assume the \ii basis.\/ $\rm A_x(0)$
and the \ii induction step.\/ $\rm \forall x[A\impP A_x(\'S'\ro x)]$.
Then for any numeral
S\dots S0 we can prove $\rm A_x(S\ldots S0)$ in S\dots S0 steps without using induction.
\bigskip
The usual belief is that any number is denoted by a numeral, so that induction
applies to any number, but
as we saw in the preceding section this belief is inexpressible or meaningless.
And if this were all that there is to induction, why bother to postulate it?
\bigskip
But the use of induction goes far beyond the application to numerals.
If there were a completed infinity $\N$ consisting of all numbers, then the
axioms of \PA\ would be true assertions about numbers and \PA\ would be consistent.
\vfill\eject
It is not a priori obvious that \PA\ can express combinatorics, but
this is well known thanks to G\"odel's great paper
on incompleteness. As a consequence, exponentiation~$\uparrow$
and superexponentiation~$\Uparrow$ can be defined in \PA\ so that we have
\nok// 15. $x\uparrow 0=\'S'0$
\nok// 16. $x\uparrow\'S'y=x\.(x\uparrow y)$
\nok// 17. $x\Uparrow0=\'S'0$
\nok// 18. $x\Uparrow\'S'y=x\uparrow(x\Uparrow y)$
\noin and similarly for primitive-recursive functions in general.
\vfill\eject
Finitists believe that primitive recursions always terminate; for example,
that applying \nn/ 10.--\nn/ 13. and \nn/ 15.--\nn/ 18.
a sufficient number of times,
\noj $\rm SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0\Uparrow
SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0\Uparrow
SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0\Uparrow SS0$
\noin reduces to a numeral. (Infix symbols are associated from right to left.)
But the putative number of times these rules must be applied
can only be expressed by means of a superexponential expres\-sion---the
argument is circular.
\bigskip
The objection to regarding variable-free \hfil\break
superexponential terms as denoting
numbers is not a naive feeling that they are too big. Rather, there is a
{\it structural}\/ problem with them.
\vfill\eject
\noindent{\bf Recapitulation:}
\bigskip
We take the extremal clause seriously: something is a number only if it can be proved
to be a number by (i)~zero is a number, and (ii)~the successor of a number is a number.
We cannot formalize this within any theory. Instead, we adjoin a unary predicate
symbol~$\phi$ and the axioms
\NOK/ 5. $\phi(0)$
\NOK/ 6. $\phi(x) \imp \phi(\'S'x)$.
\medskip
\noin and if we have proved $\rm\phi(d)$ we say that d~is a number. In this way
we express the extremal clause by a combination of the formal and the genetic.
\vfill\eject
We cannot prove
\noj $\phi(x_1) \and \phi(x_2) \imp \phi(x_1+x_2)$.
\medskip
That is, if we take the extremal clause at face value, we cannot prove that
the sum of two numbers is a number.
\medskip
To see this, we again argue semantically. Consider again the non-standard number~e
in our structure~$\cal A$, but now let $\cal X$~be the set of all individuals
of the form $\rm e_{\cal A} + \xi$ where $\xi$ is standard---that is, of the form
$\rm {\cal A}(S\ldots S0)$---and let~$\phi_{{\cal A}_\phi}$ be~$\cal X$. Then \hfil\break
$\rm\phi(e)$ is true in the structure but $\rm\phi(e+e)$ is not.
\bigskip
But we can do something almost as good.
\vfill\eject
Assuming the associative, distributive, and commutative laws and the usual
properties of~$\le$, we can establish the following {\it relativization scheme}.
Introduce
\nok// 19. $\phiz(x) \iff \forall y [y\le x \impP \phi(y)]$
\nok// 20. $\phio(x) \iff \forall y [\phiz(x) \impP \phiz(y+x)]$
\nok// 21. $\phit(x) \iff \forall y[\phio(y) \impP \phio(y\.x)]$.
\bigskip
Then $\phit$ is not only inductive but respects
$+$ and~$\.$ and is hereditary, and it is stronger than~$\phi$. That is, we
have the following theorem (proved without using induction, of course, which
is not available for~$\phi$).
{\openup4\jot
\nok// 22. $\phit(0) \and [\phit(x) \impP \phit(\'S'x) ] \and \hfil\break
[\phit(x_1) \andD \phit(x_2) \impP \phit(x_1+x_2) \andD \phit(x_1\.x_2)]
\AND [\phit(x) \andD y\le x \impP \phit(y)] \and \hfil\break
[\phit(x) \impP \phi(x)]$.
}
\vfill\eject
The use of relativization schemes permits an extensive development of arithmetic
staying within the world of numbers---numbers~$x$ satisfying~$\phi(x)$.
\medskip
Associativity is essential to the relativization scheme. For example,
suppose that \hfil\break
$\phi^2(x_1) \andD \phi^2(x_2)$; we want to prove $\phi^2(x_1\.x_2)$.
Suppose that $\phi^1(y)$; by \nn/ 21., we need to prove that
\noj $\phi^1\big(y\.(x_1\.x_2)\big)$.
\noin But we have $\phi^1(y\.x_1)$ by \nn/ 21. and so \hfil\break
$\phi^1\big((y\.x_1)\.x_2\big)$,
again by \nn/ 21.. By the associativity of multiplication we have the desired result.
\bigskip
Exponentiation is not associative, so we cannot extend the relativization scheme,
in the first way one would think of, to include exponentiation. In fact,
one can prove the following theorem:
\vfill\eject
{\it Let\/ \ro T be any consistent theory containing the axioms \nn/ 8.--\nn/ 13.
and\/ \nn/ 15.--\nn/ 18. (the usual axioms for\/ $0$ \ro S $+$ $\.$ $\uparrow$
and\/ $\Uparrow$) and the usual defining axiom for\/ $\le$.
Then there is no unary predicate symbol\/ $\phi^3$ in an
extension by definitions\/ $\rm T'$ of\/ $\rm T^\phi$ such that}
{\openup4\jot
\nok// 23. $\vdash_{\ro T'}\ \phie(0) \and [\phie(x) \impP \phie(\'S'x) ] \and \hfil\break
[\phie(x_1) \andD \phie(x_2) \impP \phie(x_1+x_2) \andD \phie(x_1\.x_2) \andD \hfil\break
\phie(x_1\uparrow x_2)] \and \hfill\break
[\phie(x) \andD y\le x \impP \phie(y)] \and \hfil\break
[\phie(x) \impP \phi(x)]$.
}
\bigskip
That is, we cannot construct a world of numbers, within the world of those
satisfying the extremal clause (those satisfying $\phi$), that is closed
under exponentiation. If the extremal clause is taken seriously,
the conclusion is that exponentiation is not total.
\vfill\eject
The proof is based on a study of the algorithm for eliminating special
constants in the proof of the Hilbert-Ackermann Consistency Theorem.
This algorithm is essentially a quantifier-elimination procedure, and it is
superexponentially long but only superexponentially long.
\bigskip
The method of proof also yields this:
\medskip
{\it With the same hypotheses, there is no unary $\phif$ such that}
\nok// 24. $\vdash_{\ro T'}\ \phif(0) \and [\phif(x) \impP \phif(\'S'x) ]
\and [\phif(x) \impP \phi(\'SS'0\Uparrow x)]$.
\bigskip
If we take the extremal clause seriously, the conclusion is that even
if $2\Uparrow \ro d$ happens to be a number, satisfying $\rm \phi(2\Uparrow d)$,
there is no general method for proving that the same holds for~$\rm2\Uparrow Sd$.
That is, there is no reason to believe that every explicit superexponential
recursion terminates.
\vfill\eject
\centerline{\bigrm The Goal}
\bigskip
The goal is to produce an explicit superexponentially long recursion and
prove that it does not terminate, thereby disproving Church's Thesis from
below, demonstrating that finitism is untenable, and proving that Peano
Arithmetic is inconsistent.
\bigskip
Do you wish me luck?
\vfill\eject
Material relevant to this talk is in {\it Predicative Arithmetic}, posted
online at
\yy
\noin \pdfklink{www.math.princeton.edu/~nelson/books/pa.pdf}{www.math.princeton.edu/~nelson/books/pa.pdf}
\bigskip
This talk is posted at
\noin {\tt www.math.princeton.edu/~nelson/papers/hm.pdf
\zz
\bye