Take the [Hilbert Basis Theorem](https://en.wikipedia.org/wiki/Hilbert%27s_basis_theorem) over the rational numbers in this form in the language of [Second Order Arithmetic](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Elementary_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/.

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](https://doi.org/10.2307/2274585), [JSTOR](https://www.jstor.org/stable/2274585)