[FOM] Conservation and Ideals

[Stephen G Simpson]

Adam Epstein <adame at maths.warwick.ac.uk> writes:
 > This brings to mind a question I recently wondered about. Namely, is the
 > Hilbert Basis Theorem provable in PA. Clearly one must do a little bit of
 > coding, and the full statement (finite generation for all ideals - say for
 > polynomial rings over Z or the algebraic numbers). However, one could
 > certainly consider a schema asserting finite generation for all
 > recursively generated ideals. Are these assertions theorems of PA?
 > 
 > Adam Epstein
 > Mathematics Institute
 > University of Warwick
 > Coventry, UK

The Hilbert Basis Theorem for PA-definable ideals is provable in PA.
The Hilbert Basis Theorem for recursively generated ideals in
polynomial rings over number fields, etc, is provable from axioms much
weaker than full PA.

This kind of question (namely, which axioms are needed in order to
prove X, where X is a specific core mathematical theorem) is dealt
with in a program of foundational research that goes under the name
"reverse mathematics".  The standard reference on reverse mathematics
is my book Subsystems of Second Order Arithmetic.  See
http://www.math.psu.edu/simpson/sosoa/.

One can attempt a reverse mathematics analysis of any specific core
mathematical theorem whatsoever.  As it happens, I have published a
paper which gives a precise and fairly satisfying reverse mathematics
analysis of the Hilbert Basis Theorem, namely

     Stephen G. Simpson, Ordinal numbers and the Hilbert Basis
     Theorem, Journal of Symbolic Logic, 53, 1988, pp. 961-974.
    
A related problem which remains open is to perform a similar analysis
of the Ritt Basis Theorem in differential algebra.

-- Steve

Stephen G. Simpson
Professor of Mathematics
Pennsylvania State University
mathematical logic, foundations of mathematics