[FOM] Hilbert's proof

[Timothy Y. Chow]

Simpson's results on Hilbert's basis theorem are very interesting in their 
own right, but I confess that I do not understand what they have to do 
with the question of the supposed "non-constructiveness" of Hilbert's 
proof, as that question is usually understood.  Provability in this or 
that subsystem of second-order arithmetic doesn't have much to do with 
constructiveness, does it?  Using classical logic, one can prove the 
existence of something in a very weak system without giving any indication 
of how to "construct" it.  Conversely, is there any reason to suppose that 
if a statement is unprovable in RCA_0 (say) then it is "non-constructive"?

In the case of Hilbert's basis theorem, a "constructive" proof would 
presumably mean one that explains how to take a "given" ideal and find a 
finite set of generators for it.  But for this to make sense as a 
question, the ideal must be "given" in some infinitary form, or some 
inexplicit form.  And if we allow that then we are implicitly allowing 
ourselves some flexibility in our definition of what constitutes a 
concrete construction.

Tim