Weakest axiom to make ZFC+X imply GCH?

Question

What is the weakest axiom $X$ that we can add to $ZFC$ to enable $GCH$ to be proven? Obviously we could just add $GCH$ but because $ZF\vdash GCH\implies AC$ that makes $AC$ redundant. So $X$ would have the properties that $ZF\vdash AC+X\implies GCH$ but $ZF\nvdash GCH\implies X$. Is such an $X$ known?

Answer 1

I think that your question is inherently problematic. We can't quite say "weakest".

It can be $V=L[A]$ for some $A\subseteq\omega_1$, but that's not right since we have models of $\sf GCH$ which are not of this form (e.g. start with $L$ and add a single Cohen subset to some regular $\kappa>\omega_1$, or to all of them).

Requiring $\sf HOD$ is too weak, since it is known that $\sf HOD$ need not imply $\sf GCH$, but we can do all sort of crazy shenanigans and still have $\sf GCH$ around.

We can also always force $\sf GCH$ by collapsing cardinals. Perhaps a proper class of them. Which can completely mess up most "nice definability axioms".

So you end up with $X$ being a very nondescript axiom, which may or may not be just $\sf GCH$ itself again, or something equivalent to it (e.g. $\lozenge$ exists for all regular cardinals+$\sf SCH$ or something like that).