How hard must "no high-degree irreducibles" proofs be? Let $\mathsf{RCF}$ be the usual theory of real closed fields and for $n>2$ let $\theta_n$ be the sentence "No degree-$n$ polynomial is irreducible." Since $\mathsf{RCF}$ is complete, for every $n$ we have $\mathsf{RCF}\vdash\theta_n$. I'm curious how hard it must be to prove $\theta_n$, as a function of $n$.
One way to formalize this is the following. Let $\mathsf{RCF}_k$ be the (finitely axiomatizable!) subtheory of $\mathsf{RCF}$ gotten by restricting attention to polynomials of degree $\le k$. Then we can ask:

What is the growth rate of the function $$\mathfrak{F}:\mathbb{N}_{>2}\rightarrow\mathbb{N}:n\mapsto\min\{k:\mathsf{RCF}_k\vdash\theta_n\}$$ sending each degree above $2$ to the highest degree we need to consider?

I'm also interested in the qualitative question, "As $n$ increases, does $\theta_n$ get meaningfully harder to prove or does the same basic strategy work for all $n$?," but I'm a bit skeptical that that's sufficiently clear to have a good answer. I'd also be interested in questions about proof length (measured either in symbols or in steps), but there I'm skeptical that there is much that's easy to say (questions about proof length tend to get hairy, in my admittedly-limited experience).

To clarify, the axiomatization I have in mind is the conjunction of

*

*the field axioms,


*the assertion that the relation "$b-a$ has a square root" is a compatible ordering, and


*for each $n$ the assertion that every degree-$n$ polynomial satisfies the intermediate value theorem.
Only this last clause is affected by the $\mathsf{RCF}\leadsto\mathsf{RCF}_k$ truncation.
 A: I don’t know how to make use of the full power of the intermediate value theorem, hence I will work instead with a weaker axiomatization: let $\def\rcf{\mathrm{RCF}}\rcf'_k$ denote the first two groups of axioms from the question (i.e., $\rcf_1$) + the assertion that every polynomial of odd degree $d\le k$ has a root, and let
$$\def\fF{\mathfrak F}\fF'(n)=\min\{k:\rcf'_k\vdash\theta_n\},\quad n>2.$$
Since $\rcf_k\vdash\rcf'_k$, we have $\fF(n)\le\fF'(n)$. (On the other hand, $\bigwedge_{n=3}^k\theta_n$ implies $\rcf_k$ over $\rcf_1$, hence $\rcf'_{\max\{\fF'(n):3\le n\le k\}}\vdash\rcf_k$. I don’t know if one can do better.)
I claim that if $n$ is not a power of $2$, then
$$\fF(n)\le\fF'(n)\le\binom n{n_2},\quad\text{where }n_2=2^{v_2(n)}$$
(i.e., $n_2$ is the highest power of $2$ that divides $n$). Note that $\binom n{n_2}$ is odd (see e.g. Kummer’s theorem).
To see this, let $R\models\rcf'_k$ for $k=\binom n{n_2}$, and assume for contradiction that $f\in R[x]$ of degree $n$ is irreducible. Let $\{\alpha_i:i\in[n]\}$ list the roots of $f$ in a fixed splitting field of $f$ over $R$.
For any symmetric polynomial $s\in R[x_1,\dots,x_{n_2}]$, the coefficients of
$$p_s(x)=\prod_{i_1<\dots<i_{n_2}}(x-s(\alpha_{i_1},\dots,\alpha_{i_{n_2}}))$$
are symmetric polynomials in the $\alpha_i$’s, hence $p_s\in R[x]$. Since $p_s$ has degree $k$, it has a root in $R$: i.e., there is $\{i_1,\dots,i_{n_2}\}\subseteq[n]$ such that
$$s(\alpha_{i_1},\dots,\alpha_{i_{n_2}})\in R.$$
Let $\{\sigma_t:t\le n_2\}$ denote the elementary symmetric polynomials in $n_2$ variables. For each $I=\{i_1,\dots,i_{n_2}\}\subseteq[n]$, $i_1<\dots<i_{n_2}$, the set
$$V_I=\bigl\{(r_1,\dots,r_{n_2})\in R^{n_2}:\textstyle\sum_tr_t\sigma_t(\alpha_{i_1},\dots,\alpha_{i_{n_2}})\in R\bigr\}$$
is an $R$-linear space, and by what we have just proved above,
$$R^{n_2}=\bigcup_{\substack{I\subseteq[n]\\|I|=n_2}}V_I.$$
Since a linear space over an infinite field is not a finite union of proper subspaces (see e.g. this question), there is $I=\{i_1,\dots,i_{n_2}\}$ such that $V_I=R^{n_2}$. That is, $\sigma_t(\alpha_{i_1},\dots,\alpha_{i_{n_2}})\in R$ for all $t=1,\dots,n$, which means that
$$\prod_{j=1}^{n_2}(x-\alpha_{i_j})\in R[x],$$
contradicting the irreducibility of $f$ (as $n_2<n$ by assumption).
Note that what we have really shown is that $\rcf'_k$ proves that every polynomial of degree $n$ has a factor of degree $n_2$.

What about the case when $n$ is a power of $2$? In the comments, I gave an argument that
$$\fF'(n)\le\frac{n!}{2^{v_2(n!)}}=\frac{n!}{2^{n-1}},$$
but this is considerably larger than the bound in the non-power-of-$2$ case. Let me outline how to prove an asymptotically better bound
$$\fF'(n)\le\binom{\binom n{n/2}}2.$$
Let $\def\acf{\mathrm{ACF}}\acf_k$ denote the theory of fields such that every polynomial of degree $2$ or of odd degree $d\le k$ has a root.
If $R\models\rcf'_{\binom{2k}2}$ then $R(i)\models\acf_k$: $\rcf'_1$ already implies that $R(i)$ is quadratically closed, and if $f\in R(i)[x]$ is a degree-$d$ polynomial with $d$ odd, then $f\overline f\in R[x]$ has degree $2d$, hence as we have shown, $\rcf'_{\binom{2d}2}$ ensures that it has a quadratic factor in $R[x]$, hence a root in $R(i)$.
By the same reasoning as above, $\acf_{\binom n{n_2}}$ proves that any degree-$n$ polynomial has a degree-$n_2$ factor. In particular, if $n\equiv2\pmod4$, then $\acf_{\binom n2}$ proves that any degree-$n$ polynomial has a root.
If $n$ is a power of $2$, then $\acf_{\binom{\binom n{n/2}}2}$ proves that any polynomial $f$ of degree $n$ has a factor of degree $n/2$, hence, by induction on $n$, it proves that any such polynomial has a root: we do the construction above with $n/2$ in place of $n_2$; since $\binom n{n/2}\equiv2\pmod4$, all the degree-$\binom n{n/2}$ polynomials considered have roots by the previous paragraph.
Now, let $n\ge4$ be a power of $2$, and $f\in R[x]$ of degree $n$, where $R\models\rcf'_{\binom{\binom n{n/2}}2}$. Doing again the symmetric polynomial construction with $n/2$ in place of $n_2$, each of the relevant degree-$\binom n{n/2}$ polynomials has a quadratic factor over $R$, hence a root in $R(i)$. In this way, we find a degree-$n/2$ polynomial $g\in R(i)[x]$ such that $g\mid f$. Since $2\binom{\binom{n/2}{n/4}}2\le\binom n{n/2}$, we have $R(i)\models\acf_{\binom{\binom{n/2}{n/4}}2}$, thus by the previous paragraph, $g$ has a root in $R(i)$, hence $f$ has a root or a quadratic factor over $R$.
