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 https://mathoverflow.net/questions/85836/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.