A famous theorem of Tarski (proved in ZF) says that, if $\mathfrak{m}^2=\mathfrak{m}$ for every infinite cardinal $\mathfrak{m}$, then the Axiom of Choice holds.
Consider the language $\{\in,F\}$, where $F$ is a binary function symbol, and let $T$ be the theory ZF+"$F$ is a bijection". Informally, $V\times V\approx V$ (where $X\approx Y$ means that there is a bijection $X\to Y$).
By standard arguments, $L$ is a model of $T$, so $T$ is consistent.
My questions are:
- Does $T\vdash$ AC?
- Does $V\times V\approx V$ reflect to any initial segment of the universe? Or to any cardinal?
- Does $T\vdash$ Global Choice? (there's an issue here regarding how to state Global Choice in a first order fashion, but still)
ZF can prove that such a bijection exists (that is, there is a specific class function it can prove is a bijection). There are obvious injections $V\times V\to V$ (the inclusion) and $V\to V\times V$ ($a\mapsto(a,\emptyset)$, say). Schroder-Bernstein can then combine these two injections to get a bijection (a little care is needed to carry out the proof of Schroder-Bernstein for classes; see this answer for one way to do it).
Since you asked about initial segments of the universe, I would add that the same argument gives that there is a bijection between $V_\alpha\times V_\alpha$ and $V_\alpha$ for all limit ordinals $\alpha$ (and that in fact there is such a bijection that is uniformly definable in $\alpha$). It follows that such a bijection also exists when $\alpha$ is an infinite successor, since if $X$ is infinite then $X\times X\approx X$ implies $X\times 2\approx X$ by Schroder-Bernstein and so $2^X\times 2^X\approx 2^{X\times 2}\approx 2^X$.