[FOM] Hilbert's proof
Timothy Y. Chow
tchow at alum.mit.edu
Tue Mar 16 13:31:06 EDT 2010
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
More information about the FOM
mailing list