Assume AC is false. (AC = axiom of choice )
Let $n,m$ be positive integers. Let $f: \Bbb N \rightarrow \Bbb N$ and $f(m)=m$.
Let $g(n,m)=1$ if the iterations $f(n),f(f(n)),...$ converges to $m$.
If $g(n,m)=1$, let $G(n,g)=x$ be the (min) amount of iterations needed to arrive at $m$.
Statement : If one can prove that $g(n,m)=1$ for all $n$ then one can prove an upper boundary $T(n)$ for $G(n,g)$.
For example if one could prove Collatz :
$g(n,1)=1$ is true for all $n$ <=> Collatz is true.
$\implies G(n,g) < T(n)$ and $T(n)$ equals (for example) $2^{2^{2^n}}$
This statement comes from someone I know, and I was not able to find a counterexample. Im not sure if this statement is a named conjecture or theorem yet.
And I do not know if its true of course.
I do know however that ZFC is required to prove Goodstein's theorem and there is no upper bound known for $G(n,g)$ here. So I think if AC is true then the statement is false.
I considered this statement to be an axiom too , but that would mean it cannot be proved or disproved which I doubt. But who knows.
Note that using $f$ as an additional symbol, one can write the definition of $g$ as a first-order statement, as well the definition of $G$ (note that $g$ is not really a variable, because $g$ itself is definable from $f$).
The statement, if so, about $T(n)$, is all but a first-order statement in the augmented language of the natural numbers.
Shoenfield's absoluteness theorem tells us that first-order statements (and even simple second-order statements) are absolute between any two models of $\sf ZF$ which have the same ordinals. That is, the statement is true in one model if and only if it is true in another.
Now, if $V$ is any model of $\sf ZF$ then $L\subseteq V$ is an inner model of $V$ satisfying the axiom of choice, so if the statement is provable from $\sf ZFC$ then it is true in $L$, and by absoluteness, it is true in $V$ as well.