[FOM] Hilbert's proof

[Alasdair Urquhart]

> > 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),
pp. 961-974.