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](https://www.ps.uni-saarland.de/Publications/documents/KirstSmolka_2017_Categoricity.pdf) 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 question about Second-Order ZF and the Axiom of Choice
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.


