Take the Hilbert Basis Theorem over the rational numbers in this form in the language of Second Order Arithmetic: For every $n\in N$ every ideal of the polynomial ring $\mathbb{Q}[x_1,\dots,x_n]$ is finitely generated. Simpson has shown this is stronger than Exponential Function Arithmetic (EFA). He proved much more on the subject but this is what interests me. I expect the statement gets weaker if you specify $n$. Is that right? So for example it would take less to prove every ideal of $\mathbb{Q}[x_1,\dots,x_4]$ is finitely generated.
Maybe the statement does not get weaker when you specify $n$, since the number of generators of ideals remains unbounded. See answers to the question Number of generators of an ideal in a polynomial ring over a Noetherian ring.
Is it known how strong the theorem is for specific $n$, or at least for some low specific $n$?
The reference for Simpson is
- "Ordinal Numbers and the Hilbert Basis Theorem," The Journal of Symbolic Logic, Sep., 1988, Vol. 53, No. 3 (Sep., 1988), pp. 961-974. doi:10.2307/2274585, JSTOR
