[FOM] Hilbert's proof

[Stephen G Simpson]

Hilbert's proof of the Hilbert Basis Theorem is famously
nonconstructive.  Therefore, from a
historical/philosophical/foundational standpoint, it is interesting to
ask about the metamathematical aspects or "logical strength" of this
theorem.

Many precise questions can be formulated.  My old paper on this
subject is

   @Article{ordinal,
     author =    "Stephen G. Simpson",
     title =     "Ordinal numbers and the {H}ilbert basis theorem",
     journal =   "Journal of Symbolic Logic",
     year =      1988,
     volume =    53,
     pages =     "961--974"
   }

There I proved the following result concerning the Hilbert Basis
Theorem.  Let $x_1,\ldots,x_n,\ldots$ be commuting indeterminates.
The following statements are pairwise equivalent over RCA$_0$.

 1. For each $n$, every ideal in the polynomial ring
    $Q[x_1,\ldots,x_n]$ is finitely generated.  Here $Q$ is the field
    of rational numbers.

 2. For each $n$ and each countable field $F$, every ideal in the
    polynomial ring $F[x_1,\ldots,x_n]$ is finitely generated.

 3. The standard notation system for the ordinal numbers up to
    $\omega^\omega$ is well ordered.

I also obtained an analogous result concerning the Robson Basis
Theorem.  Here $x_1,\ldots,x_n,\ldots$ are noncommuting
indeterminates, and the appropriate ordinal number is
$\omega^{\omega^\omega}$ rather than $\omega^\omega$.  Thus we see
that the Robson Basis Theorem is strictly and measurably "stronger" or
"more nonconstructive" than the Hilbert Basis Theorem.

A still-open question is to measure the strength of the Ritt Basis
Theorem.  Here $x_1,\ldots,x_n,\ldots$ are commuting differential
indeterminates.

Those who wish to discuss the speculative or philosophical aspects of
these matters are encouraged to do so.

Stephen G. Simpson
Professor of Mathematics
Pennsylvania State University
http://www.math.psu.edu/simpson/

Research interests: foundations of mathematics, mathematical logic.