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.