[FOM] 175:Maximal Principle/Hilbert's Program

[Harvey Friedman]

INDUCTION AND MAXIMALITY IN ARITHMETIC
Harvey M. Friedman
June 4, 2003
DRAFT

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

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" 
comprehensions.

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 
envisioned?

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 
incompleteness theorem.

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 
manuscript

H. Friedman, Finite reverse mathematics, October 19, 2001, 
http://www.mathpreprints.com/math/Preprint/show/

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. 
235-242.

H. Friedman, Systems of second order arithmetic with restricted 
induction, I,II (abstracts), Journal of Symbolic Logic 41 (1976), 
557-559.

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

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 
variable x.

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

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

1. DOR.
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 
undefined.

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 
Axy+Bxz+Cxw+Dxu+Eyz+Fyw+Gyu+Hzw+Izu+Jwu+Kx+Ly+Mz+Nw+Ou+P, with 
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 
0.

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 
Axy+Bxz+Cxw+Dxu+Eyz+Fyw+Gyu+Hzw+Izu+Jwu+Kx+Ly+Mz+Nw+Ou+P-k.

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 
function arithmetic.

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 
of n!.

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.

1. DOR.
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

1. DOR.
2. PELL.
3'. The values of every quadratic in any number of variables, with 
variables restricted to intervals, contains a maximum interval about 
0.

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

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

Harvey Friedman