A question about Second-Order ZF and the Axiom of Choice This question follows Noah Schweber's excellent answer to a corresponding question regarding second-order $ZFC$ and the continuum hypothesis: https://mathoverflow.net/a/78083/24611
Simply put, it seems that $ZFC_2$ "decides" $CH$ in a certain sense that can be made formally precise, although second-order logic is so limited as to make it impossible for us to determine which way it is decided. This seems, if my understanding is correct, to be related to $ZFC_2$ being categorical if large cardinals are excluded.
Does a similar situation exist for $ZF_2$ and $AC$?
This paper seems to show that it is, and that $ZF_2$ is likewise categorical if large cardinals are excluded. Hence, this would mean that we have the same analogous situation to with $ZFC_2$ and $CH$, so that $AC$ is likewise "decided" in $ZF_2$, but that we don't know which way it is decided.
Is this analogy correct?
 A: 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.

