FOM: Applications of formal systems of reverse mathematics

[Harvey Friedman]

Various formal systems are used in the development of Reverse Mathematics.
These formal systems have been intensively studied for various purposes,
including but not limited to Reverse Mathematics. Simpson's book, as can be
seen from its title, covers not only Reverse Mathematics but the study of
these formal systems as well.

Some people consider the study of these formal systems as part of Reverse
Mathematics. But I like to preserve the distinction, because if that
distinction is adhered to, then the value and precise scope of Reverse
Mathematics is much easier to state. Obviously Reverse Mathematics would be
a larger subject if it included the study of such systems for their own
sake or for other purposes. But I will adhere to the distinction, whereby
Reverse Mathematics is very focused and very specific.

Here are some "hard" applications of formal systems associated with reverse
mathematics to problems of some interest to a variety of mathematicians.
They are "hard" in that they are used to derive statements that do not
mention the formal systems in question.

The applications presented here all take the form of an upper bound
associated with a simple mathematical context. The upper bound is obtained
as an application of formal systems by first proving the appropriate
existence statement in one of the formal systems. Then one applies a
general theorem about that formal system that provides an upper bound for
any provable existential statement. In each case, the method can very
likely be removed, although it is not clear what complexities emerge when
actually doing this. And it is likely that one could get sharper upper
bounds by removing the method. So it is a worthy project to eliminate the
method. However, it seems that the simplest way of getting such upper
bounds is to use the method.

Of course, I emphasize that the main application of formal systems is to
issues in f.o.m. and f.o.m. driven investigations such as reverse
mathematics. I expect this to be the case for the forseeable future.

Put differently, the study of these formal systems already has an entirely
convincing motivation that fits squarely into the general intellectual
interest framework. It doesn't need applications of this sort - or any
related sort - to justify intense investigation.

1. HILBERT'S SEVENTEENTH PROBLEM

We discuss one form of Hilbert's 17th problem which immediately lends
itself to questions of bounds. This was proved by E. Artin:

THEOREM 1.1. Let P be a polynomial of several variables with rational
coefficients. Suppose that P is nonnegative over the reals. There exists
polynomials Q1,...,Qn,R1,...,Rn with rational coefficients, n >= 1, where
the R's are not the zero polynomial, such that the equation P = (Q1/R1)^2 +
... + (Qn/Rn)^2 is true over the reals. I.e., every positive definite
polynomial with rational coefficients can be written as a sum of squares of
polynomials with rational coefficients.

[More general things were proved by Artin; e.g., replace rationals with any
subfield of the reals. And Artin proved a uniform version of this with
"weights"].

Define the size of a polynomial of several variables with rational
coefficients to be the maximum of the absolute values of the numerators and
denominators of the coefficients in reduced form, the degree, and the
number of variables.

For each n >= 0 let H(n) be the least m such that every positive definite
polynomial with rational coefficients of size at most n can be written as a
sum of squares of polynomials with rational coefficients of size at most
f(n).

Historically, people have been interested in the growth rate of H and
related functions associated with Hilbert's 17th problem. It is easy to see
that such answers are essentially equivalent to a classification of the
computational complexity of H itself, and we phrase the results in these
terms.

Abraham Robinson observed that using Tarski's decision procedure for real
closed fields, H is a recursive function. Even this is not obvious to a
general mathematician unless they are used to thinking in recursion
theoretic terms.

According to my understanding of the situation, the lower bounds are
virtually nonexistent. E.g., H might be polynomially bounded! I don't
recall even seeing a proof that H is not linearly bounded.

As our first application of formal systems,

**H is primitive recursive**

Actually, this is an application of one of the five basic systems of
reverse mathematics called RCA0 + WKL. In Simpson's book, it is called
WKL0. It is the second in the standard list of five. [WKL stands for "weak
Konig's lemma" which asserts that any infinite 0-1 tree has an infinite
path].

One first develops the Artin theory of real fields in RCA0 + WKL. This is
discussed in Simpson's book, although some details are not fully
explicated. I know how to do this, and am working out the details for doing
this in a much weaker system as indicated below. In particular, one proves
Theorem 1.1 in the following purely pi-0-2 form within RCA0 + WKL.

THEOREM 1.1'. Let P be a polynomial of several variables with rational
coefficients. Suppose that P is nonnegative over the rationals. There
exists polynomials Q1,...,Qn,R1,...,Rn with rational coefficients, n >= 1,
where the R's are not the zero polynomial, such that the equation P =
(Q1/R1)^2 + ... + (Qn/Rn)^2 is formally true. I.e., when clearing
denominators one gets a formal identity between two polynomials.

These proofs follow the usual algebraic proofs but require some more care.

We now apply the following metatheorem. See Simpson's book, page 381:

THEOREM 1.2. If a pi-0-2 sentence is provable in RCA0 + WKL then it has a
primitive recursive witness function. In fact, there is a specific
primitive recursive function for which it is provable in PRA (primitive
recursive arithmetic) that it is a witness function.

So then we get a primitive recursive witness function for Theorem 1.1', and
hence for Theorem 1.1. I.e.,

*The function H is primitive recursive.*

Many years ago, Kreisel published an abstract in 1974 sketching an argument
using proof theory and algebra that there is an indefinitely iterated
exponential bound instead of just a primitive recursive bound. There is an
extended criticism of this argument as well as a later unpublished sketch
of mine that there is an iterated exponential bound - around a stack of 10
2's - in the long article by Delzell in the Kreisel volume edited by
Odifreddi which also discusses results by various other people going in
other directions.

These arguments use proof theory of systems without quantifiers over sets,
rather than more mathematically congenial arguments involving subsystems of
second order arithmetic such as the one sketched above for merely a
primitive recursive upper bound. In particular, my sketch used a nonobvious
refinement of the cut elimination theorem for predicate calculus. My sketch
as well as other sketches of bounds - including Kreisel's - have been
criticized in various justified ways, and I always have wanted to get back
to this to write something more definitive on the matter.

I am optimistic about an approach that would go a long way to cleaning up
this situation through formal systems based on WKL, avoiding any delicate
proof theoretic considerations. The approach would have several advantages,
including a byproduct for mainline f.o.m. which I will mention below.

So here is the plan. When I have carried it out, I will post it in my list
of positive postings with considerable details - this is, after all, a
rather treacherous area, as can be seen by the Delzell article cited above.

The relevant formal system to use is RCA0* + WKL = WKL0* as defined on page
410 of Simpson's book. This is yet another formal system associated with
reverse mathematics.Simpson/Smith

*Factorization of polynomials and Sigma-0-1 induction, Annals of Pure and
Applied Logic 31 (1986), 289-306*

published on the RCA0* and WKL0*, and in particular proved the following
conservation result:

THEOREM 1.3. If a pi-0-2 sentence is provable in RCA0* + WKL then it has an
elementary recursive witness function. In fact, there is a specific
elementary recursive function for which it is provable in EFA (elementary
recursive arithmetic) that it is a witness function.

The plan is to prove Theorem 1.1' in RCA0* + WKL, and in fact develop the
Artin theory of real fields in RCA0* + WKL. Two byproducts of this plan
will be the following:

A. The function H defined above is elementary recursive.

And this byproduct for f.o.m.:

B. EFA proves the consistency of the first order theory of real closed fields.

This is much easier to carry out for the first order theory of
algebraically closed fields.

Of course, one would need more in order to get an upper bound on the height
of the exponential stack in the upper bound. E.g., my old sketch claimed
about height 10. Nevertheless, this plan should result in a proof of much
greater clarity and acceptance than my original manuscript.

2. FINITE FORM OF HILBERT'S BASIS THEOREM

Simpson proved that the Hilbert basis theorem for polynomials of several
variables over countable fields is equivalent to

omega^omega is well ordered

over RCA0. Also, he proved that in each fixed number of variables is
provable in RCA0.

Later I formulated and proved a finite form of the Hilbert basis theorem:

*) Let n >> k,p >= 1 and I1 properlycontainedin I2 properlycontainedin ...
properlycontainedin Im be ideals in the polynomial ring in k variables over
any field, where each Ij has generators of degree at most j+p. Then m <= n.

Let H(k,p) be the least n such that this statement holds. By using
Simpson's result and my proof of *), it is clear that for each k, the
finite form is provable in RCA0 + WKL. This is again that second system of
reverse mathematics in the hierarchy of five. This yields a primitive
recursive upper bound for the >> in *) for any fixed number of variables,
k, at least for finite fields (and some other fields and rings). Some other
machinations will get these primitive recursive bounds to hold for *) as
written, uniformly over all fields.

There are lower bounds that go cofinally up through the hierarchy of
primitive recursive functions, even for the 2 element field.

This finite form of Hilbert's basis theorem was discussed, essentially, by
Siedenberg, and only in the case of quite small dimensions (number of
variables). He gave a complicated proof of it - far more complicated than
my proof of *) using basic logic, and only in small dimensions.

3. DECREASING CHAINS OF ALGEBRAIC SETS

In my posting of 2:56PM 5/25/99, I considered related finite forms of
Hilbert's basis theorem, relating to decreasing chains of algebraic sets.
The fact that there is no strictly decreasing sequence of algebraic sets
over the complexes or reals (or any field) is a well known important
consequence of the Hilbert basis theorem. The primitive recursive bounds
there can be most easily obtained in the same way that the results of the
previous section are most easily obtained.

4. There are other situations of this rough kind where the formal systems
of reverse mathematics or other formal systems can be used to rather easily
give upper bounds. I hope to report on some other ones later.