Let me start by observing that we have to be a bit careful when talking about ZF$_2$. Specifically, there is a subtle distinction between set models and class models which needs to be highlighted. In one sense, ZF proves that $V$ is a class model of ZF$_2$ - in another sense, it can't even express this claim appropriately. For this reason I'm going to take as our background theory NBG$^\circ$ = NBG without global choice *(or any choice - I don't think this notation is standard but I haven't seen a notation for it)*, and use the word "model" to refer to *class models* (note that every set model is a class model).

Now NBG$^\circ$ proves the following key fact:

Every model of ZF$_2$ is isomorphic to a unique initial segment of the cumulative hierarchy (possibly the whole thing). Moreover, the set models of ZF$_2$ are exactly the levels $V_\kappa$ for $\kappa$ strongly inaccessible. Finally, there exists at least one model of ZF$_2$ (namely, $V$ itself).

Proving this is straightforward: first show that models of ZF$_2$ are well-founded, next show via second-order powerset that they "get powersets right," and finally show via second-order replacement that the height of any such model must be either an inaccessible cardinal or $Ord$ itself.

We can now make the following argument in NBG$^\circ$, as per the linked question:

- The following are equivalent: $(i)$ CH. $(ii)$ Every model of ZF$_2$ satisfies CH. $(iii)$ Some model of ZF$_2$ satisfies CH.

The strength of $(iii)$ here comes from the fact that CH is a "bounded statement:" it only refers to objects of fixed finite order. By contrast, a failure of choice could occur for the first time very high in the cumulative hierarchy. NBG$^\circ$ **can** prove:

- Suppose AC. Then every model of ZF$_2$ satisfies AC.

*Proof*. If $x$ is well-orderable, then a well-ordering of $x$ exists in the powerset of $x\times x$. Now simply use that ZF$_2$-models are closed under true powersets. $\quad\Box$

The converse, however, can fail. Let $M$ be a model of NBG$^\circ$ + "There is an inaccessible cardinal" + "Choice holds below the first inaccessible" + "$\neg$AC." (Such an $M$ exists iff NBG + "There is an inaccessible cardinal" is consistent iff ZF + "There is an inaccessible cardinal" is consistent.) Then:

- We have $M\models$ "There are models of ZF$_2$ that disagree about AC."

Namely, $(V_\kappa)^M$ thinks AC is true while $V^M$ thinks AC is false (here $\kappa$ is the least inaccessible in $M$). Note that $V^M$ isn't quite $M$ itself, but rather the *sets-part* of $M$ ($M$ is a model of NBG$^\circ$, not ZF).

On the other hand, of course, the inaccessible is necessary. In NBG$^\circ$ we can prove (as an easy corollary of the bolded claim up at the top of this answer):

- If there is no inaccessible cardinal, then there is exactly one model of ZF$_2$ - namely, $V$.

Consequently, we have:

- If there is no inaccessible cardinal, then ZF$_2$ is categorical
*(in the sense of class models - it's unsatisfiable in the sense of set models)* and hence decides AC.

doesn'tdecide AC, since there are models of $ZF_2$ it which it does or doesn't hold? (the same couldn't have happened for CH, since the failure is always determined below the first inaccessible) $\endgroup$ – Wojowu Apr 15 '18 at 18:55