[FOM] Hilbert's proof
urquhart at cs.toronto.edu
Tue Mar 9 11:34:17 EST 2010
> > What was an essence of the "totally new method" by which Hilbert could
> > prove his the existence of a finite basis for the invariant forms?
> > with reagards, adam
> It was non-constructive. There is a reasonable brief discussion of this on
> Wikipedia: http://en.wikipedia.org/wiki/David_Hilbert#The_finiteness_theorem
I think it depends on what you mean by "non-constructive". Hilbert's
second proof is, I believe, formalizable in the theory RCA_0 +
"omega^omega is well-ordered." It is not provable in RCA_0.
For these and other results see Steve Simpson's fine article
"Ordinal Numbers and the Hilbert Basis Theorem", JSL Volume 53 (1988),
More information about the FOM