Take the Hilbert Basis Theorem over the rational numbers in this form in the language of Second Order Arithmetic: For every $nin 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