[FOM] 175:Maximal Principle/Hilbert's Program
friedman at math.ohio-state.edu
Sun Jun 8 23:59:04 EDT 2003
INDUCTION AND MAXIMALITY IN ARITHMETIC
Harvey M. Friedman
June 4, 2003
Abstract. We derive a metamathematical induction principle (IDelta0
or bounded induction) from a maximality principle of a fundamental
number theoretic nature (the existence of maximal intervals in the
range of quadratics in five variables whose variables are bounded to
1. HILBERT'S PROGRAM REVISITED.
It can be argued that the formal systems studied in f.o.m.
extrapolate from mathematical practice in a way that is too general.
Sure, mathematicians use inductions, and sure mathematicians use
comprehension. However, mathematicians only use "beautiful and
productive" inductions, and only use "beautiful and productive"
Might it be possible to formalize mathematics in a more subtle way,
in which only "beautiful and productive" inductions are postulated,
and only "beautiful and productive" comprehensions are postulated?
And, if mathematics is so formalized, then perhaps it can reasonably
cover all or nearly all of "beautiful and productive" mathematics,
but still be subject to a consistency proof of the kind that Hilbert
This is not possible if the consistency proof is to be formalized in
the same system, by Godel's second incompleteness theorem.
However, the consistency proof may be carried out in, say, a weak
fragment of Peano Arithmetic, yet be UGLY. The consistency proof can
be entirely formal and carried out fully within the methods
envisioned by Hilbert, without running afoul of Godel's second
The best that we can get from Godel's second theorem is that the
consistency proof must be UGLY, but this is as expected.
We believe that even this form of Hilbert's program is impossible.
However, a refutation is a very delicate matter, and can be subject
to higher and higher standards.
This paper marks the beginning of a serious attack against this
modified form of Hilbert's program - along with the following earlier
H. Friedman, Finite reverse mathematics, October 19, 2001,
Put differently, we are mounting a serious defense of the decisive
significance of Godel's second incompleteness theorem in connection
with Hilbert's program.
The method is precisely according to what I envisioned as I started
to create what is now called "reverse mathematics", around 1969. The
following later unpublished manuscripts refer to a result from 1969,
but also is very explicit in terms of the approach:
H. Friedman, The analysis of mathematical text, and their calibration
in terms of intrinsic strength, I-IV, State University of New York at
Buffalo, April 3, April 8, May 19, August 15, 1975.
For example, in III, I wrote
"It's not what the mathematician would accept if confronted with; but
what the mathematician has accepted and been confronted with".
"We have thus associated a combinatorial structure |B| to every body
of mathematics, which we call the *raw formal system* for B."
In those early manuscripts, I tried to delve too quickly into the
realm of real analysis, having no idea how to go about things in pure
arithmetic. The work was a bit unwieldy - and ahead of its time! -
and I abandoned it in favor of the relatively self contained and
comparatively attractive approach through my base theory RCA0 and the
strategic statement of Reverse Mathematics. See
H. Friedman, Some systems of second order arithmetic and their use,
Proceedings of the International Congress of Mathematicians,
Vancouver 1974, vol. 1, Canadian Mathematical Congress, 1975, pp.
H. Friedman, Systems of second order arithmetic with restricted
induction, I,II (abstracts), Journal of Symbolic Logic 41 (1976),
H. Friedman and S.G. Simpson, Issues and problems in reverse
mathematics, in: Computability Theory and its Applications, ed.
Cholak, Lempp, Lerman, Shore, Contemporary Mathematics, vol. 257,
American Mathematical Society, 2000.
The base theory RCA0 is particularly convenient, even though it is
subject to the obvious objection that it is based on the logician's
extrapolation of mathematical practice.
In fact, my original axiomatization of RCA0 in the JSL abstracts
above attempted to address just this issue. So I avoided schemes as
in Simpson's axiomatization of RCA0, with the scheme of Sigma-0-1
induction and the scheme of Delta-0-1 comprehension. Instead, I used
much more directly mathematical axioms. However, they are still not
mathematical enough to satisfy the present emerging standards.
The essential method is to first build formal systems solely out of
mathematical statements ideally from the literature, which are
regarded as unremovable fixtures of mathematics. In order to meet
this standard, each axiom has to represent a fundamental fact that is
either a valued theorem or is at least inexorably linked with a
productive development in mathematics which has a clear permanent
place in the mathematical literature. The essential method is to then
show that such formal systems are logically equivalent to the usual
well studied formal systems of f.o.m. In some later development of
the approach, it might be sufficient to settle for mutual
interpretability rather than outright logical equivalence.
I still do not know how to accomplish to perfection. It is not clear
whether or not it can be accomplished to perfection. Perfection would
mean that one only only uses axioms that are verbatim quotes without
modification of mathematical facts that are widely used and
Another way to characterize the program is to view it as reverse
mathematics without coding. However, the requirements are more
stringent than that. I prefer to call it
*honest reverse mathematics*.
2. SOME BACKGROUND.
IDeltaD0 is usually formulated on the natural numbers, rather than on
Z. However, for our purposes, it is more natural to work on Z.
We write IDelta0(Z) for the following theory in the language
0,1,+,-,x,< of ordered rings.
1. DOR. Axioms for discrete ordered rings.
2. Bounded Induction. (phi[x/0] and (forall x >= 0)(phi implies
phi[x/x+1])) implies (forall x >= 0)(phi), where phi is Delta0.
Here the Delta0 formulas are defined from atomic formulas and
connectives, using bounded quantification:
(therexists x in [s,t])(phi), (forall x in [s,t])(phi)
where s,t are terms in the language of rings that do not mention the
The very close relationship between IDelta0 = IDelta0(N) and
IDelta0(Z) is obvious.
It is well known how to code finite sequences within IDelta0(Z),
except that we cannot prove the existence of codes for finite
sequences whose length is arbitrary.
However, using this coding apparatus, one then defines the axiom EXP,
which asserts that to every x,y >= 0 there is a unique x^y.
The system IDelta0(Z) + EXP is particularly important. There are some
alternatives to the rather technical EXP that result in the same
There is an old result of mine that over IDelta0(Z) + EXP is equivalent to
3. CM. Common multiple. For all n > 0 there exists m > 0 such that m
is a multiple of every 0 < i <= n.
Obviously CM is entirely implicit in any context where one sees n!
for positive integers n.
It is of course natural to incorporate exponentiation directly into
the axiomatization. This is normally called IDelta0(exp). The close
relationship between IDelta0(exp) and IDelta0 + EXP is well known.
We prefer to use IDelta0(Z,exp) and write the usual IDelta0(exp) as
IDelta0(N,exp). The language is 0,1,+,-,x,<, with the binary function
symbol E. Of course, in practice we write E(x,y) as x^y.
The axioms of IDelta0(Z,exp) are
2. Bounded Induction. This is expanded to accommodate the expanded language.
3. Exponentiation. x^0 = 1, y >= 0 implies x^y+1 = (x^y)x.
We have taken the approach that we leave it open as to what x^y is
when y < 0. This approach has advantages and disadvantages. Other
approaches with different advantages and disadvantages are
i) declaring a default value (normally 0) for xy when y < 0;
ii) using free logic (logic with undefined terms) and declaring that
x^y is undefined when y < 0.
Another issue is the value of 0^0, which can be argued to be 1, 0, or
None of these decisions alter the basic well known close relationship
between IDelta0(Z) + EXP and ID0(Z,exp). These are also closely
related to IDelta0(N) + EXP and ID0(N,exp).
We have forcefully conjectured that IDelta0(Z,exp) is sufficient to
prove all of the celebrated theorems of number theory.
3. NEW SYSTEM.
Intervals are given by expressions [a,b]. An interval [a,b] is said
to be about x if and only if a <= x <= b, or a > b.
1. DOR. Discrete ordered ring axioms.
2. CM. For n <= 1, 1,...,n have a nonzero common multiple.
3. RMAX. The values of the five variable quadratic
variables restricted by the inequalities a <= x <= b, c <= y <= d, e
<= z <= f, g <= w <= h, i <= u <= j, include a maximum interval about
Here RMAX means "restricted maximal principle". It is an immediate
consequence of IDelta0(Z).
It is obvious in 3 that the values there include an interval of
maximum length about any given integer k. This is because we can
simply apply 3 to
We will prove that DOR + CM + RMAX is equivalent to IDelta0(Z) + EXP.
IDelta0(Z) + EXP is perhaps the weakest fundamentally robust system
of integer arithmetic. As remarked earlier, it is equivalent to
IDelta0(Z) + CM, and to IDelta0(Z) + P. It is finitely axiomatizable.
As remarked before, ID0(Z) + EXP is conservatively extended by
IDelta0(Z,exp). The system IDelta0(N,exp) was originally formulated
by me, and called EFA = exponential function arithmetic = elementary
Note that all three axioms DOR, CM, RMAX, are explicitly given single
statements involving only familiar mathematical objects and contexts,
in which there is a highly valued body of positive mathematical
developments. In the case of DOR, this is completely evident. In the
case of CM, this is clear since CM follows immediately from any use
In the case of five variable quadratics, there is a valued body of
work starting with Carl Ludwig Seigel on the positive solution of
Hilbert's tenth problem for quadratics in any number of variables.
RMAX is implicit in any contemplation of the ranges of quadratics in
five variables, restricted or otherwise. The subject
"what do the ranges of quadratics look like"
is very appealing, and I believe will be the subject of serious
research in number theory shortly.
4. COMPARISON WITH D'AQUINO.
Paola D'Aquino, "Pell equations and exponentiation in fragments of
arithmetic" Annals of Pure and Applied Logic 77 (1996) 1-34,
considered the following system.
2. PELL. Every Pell equation has a nontrivial solution.
3. BDI. Bounded Diophantine Induction.
D'Aquino shows that this is also equivalent to IDelta(Z) + EXP. It
appears that this system is a consequence of the system
3'. The values of every quadratic in any number of variables, with
variables restricted to intervals, contains a maximum interval about
Axiom 2 is the so called Pell axiom P, and asserts that every Pell equation
x^2 - dy^2 = 1
has a solution with y not= 0, provided d is not a square.
Axiom 3' is the extension of my RMAX above to any quadratic in any
number of variables.
However, 3,3' are schemes in the language of ordered rings. One can
get some sort of bound on the number of variables that is sufficient
to get IDelta(Z) + EXP, but the bound is too large for us to
reasonably write down the corresponding axiom, which requires us to
display the appropriately generic quadratic involved. This is far too
large to be reasonable, as the proof passes through the Matijasevic
work on Pell's equation that shows that exponentiation is Diophantine.
The use of the maximum principle RMAX rather than Diophantine
induction, allows us to avoid use of Matijasevic's work on Pell's
equation, and instead to concentrate on detailed use of the much
earlier and simpler Godel beta function apparatus. This is much more
There are some open questions here.
A. Does DOR + PELL + RMAX imply IDelta0(Z)?
B. Does DOR + PELL + BDI for quadratics in 5 variables imply IDelta0(Z)?
C. Does DOR + CM + BDI for quadratics in 5 variables imply IDelta0(Z)?
I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 175th in a series of self contained numbered postings to
FOM covering a wide range of topics in f.o.m. The list of previous
numbered postings #1-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:
150:Finite obstruction/statistics 8:55AM 6/1/02
151:Finite forms by bounding 4:35AM 6/5/02
152:sin 10:35PM 6/8/02
153:Large cardinals as general algebra 1:21PM 6/17/02
154:Orderings on theories 5:28AM 6/25/02
155:A way out 8/13/02 6:56PM
156:Societies 8/13/02 6:56PM
157:Finite Societies 8/13/02 6:56PM
158:Sentential Reflection 3/31/03 12:17AM
159.Elemental Sentential Reflection 3/31/03 12:17AM
160.Similar Subclasses 3/31/03 12:17AM
161:Restrictions and Extensions 3/31/03 12:18AM
162:Two Quantifier Blocks 3/31/03 12:28PM
163:Ouch! 4/20/03 3:08AM
164:Foundations with (almost) no axioms, 4/22/0 5:31PM
165:Incompleteness Reformulated 4/29/03 1:42PM
166:Clean Godel Incompleteness 5/6/03 11:06AM
167:Incompleteness Reformulated/More 5/6/03 11:57AM
168:Incompleteness Reformulated/Again 5/8/03 12:30PM
169:New PA Independence 5:11PM 8:35PM
170:New Borel Independence 5/18/03 11:53PM
171:Coordinate Free Borel Statements 5/22/03 2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals 5/34/03 1:55AM
173:Borel/DST/PD 5/25/03 2:11AM
174:Directly Honest Second Incompleteness 6/3/03 1:39PM
More information about the FOM