Let $\mathfrak{ZFC}(\mathsf{SOL})$ be the theory in second-order logic (with the standard semantics) gotten from $\mathsf{ZFC}$ by modifying the Separation and Replacement schemes to apply to arbitrary second-order formulas. For example, for each second-order formula $\varphi$ with only first-order free variables $x\_1,...,x\_n,x\_{n+1}$ we have the Separation instance $$\forall x\_1,...,x\_n,y\exists z\forall w(w\in z\leftrightarrow w\in y\wedge \varphi(x\_1,...,x\_n,w)).$$


Note that $\mathfrak{ZFC}(\mathsf{SOL})$ is **not the same as the system called "second-order $\mathsf{ZFC}$"** - see e.g. [here](https://math.stackexchange.com/questions/3064566/what-features-of-a-logic-make-possible-the-proof-of-downward-lowenheim-skolem/3530773#3530773).


Building off of [this MSE question of mine](https://math.stackexchange.com/q/3550364/28111), I'm interested in understanding the models of this theory. I'm hoping that by restricting to levels of the cumulative hierarchy we can get a clean answer:



> 
> **Question 1**: For which cardinals $\alpha$ do we have $V\_\alpha\models\mathfrak{ZFC}(\mathsf{SOL})$?
> 
> 
> 


It's easy to show that every (strongly) inaccessible cardinal has this property; the converse, however, is not immediately clear to me. My current suspicion in fact is that (very) large cardinals imply the existence of non-inaccessible $\alpha$s with the above property, but I don't immediately see how to prove this.




---


As a secondary question, I'm also interested in a "Henkin version" of this question:



> 
> **Question 2**: For which $\alpha$ is there an $X\subseteq \mathcal{P}(V\_\alpha)$ such that $(V\_\alpha,X)$ forms a Henkin model of $\mathfrak{ZFC}(\mathsf{SOL})$?
> 
> 
> 


At a glance I think that the least such $\alpha$ has countable cofinality, by a quick modification of the analogous argument for worldly cardinals, but I haven't had time yet to check the details.



Analogues of worldly cardinals for (an unusual version of) second-order $\mathsf{ZFC}$
Complementing @JasonChen's answer: Assume ZFC+$I\_1$ and let $j:V\_{\lambda+1}\to V\_{\lambda+1}$ be elementary, so $\lambda$ is the sup of the critical sequence of $j$. Then $V\_{\lambda}$ models $\mathfrak{ZFC}(\mathsf{SOL})$, but $\mathrm{cof}(\lambda)=\omega$. For suppose $f:V\_\alpha\to\lambda$ is cofinal and definable over $V\_{\lambda+1}$ from the parameter $p\in V\_{\lambda}$. Let $n<\omega$ be such that $\alpha,p\in V\_{\mathrm{crit}(j\_n)}$
(where $j\_n=$ the $n$th iterate of $j$). Note that $j\_n\circ f\neq f$, because taking $x\in V\_\alpha$ with $f(x)>\mathrm{crit}(j\_n)$, we get $j\_n(f(x))>f(x)$. But $j\_n\circ f=f$ because $j\_n:V\_{\lambda+1}\to V\_{\lambda+1}$ is elementary and $j\_n(p,\alpha)=(p,\alpha)$.


Edit, considering @AsafKaragila's comment on consistency strength: Consistency-wise, the assumption above was overkill; a measurable suffices. Assume ZFC + $\kappa$ is measurable. Let $G$ be Prikry generic at $\kappa$. So $\kappa$ has cofinality $\omega$ in $V[G]$. Claim: In $V[G]$, $V\_\kappa$ models $\mathfrak{ZFC}(\mathsf{SOL})$. In fact, if $f:\omega\to\kappa$ is cofinal and $f$ is definable over $V\_{\kappa+1}^{V[G]}$ from parameters in $V\_\kappa$, then $f\in V$, so $f$ is bounded. Since $V\_\kappa^{V[G]}=V\_\kappa^V$, this is a consequence of the fact that $\mathrm{HOD}^{V[G]}\_V=V$, i.e. if $X\in V[G]$ and $X\subseteq V$ and $X$ is definable over $V[G]$ from parameters in $V$, then $X\in V$. (This follows from the fact that if $p,q$ are Prikry conditions then there are generics $G\_p,G\_q$ with $p\in G\_p$ and $q\in G\_q$ and $V[G\_p]=V[G\_q]$.)


Edit 2: On the other hand, the kind of argument used in the paper "Inner models from extended logics: Part 1" referred to in @JasonChen's answer to show that in $L$, $V\_\alpha$ models $\mathfrak{ZFC}(\mathsf{SOL})$ iff $\alpha$ is inaccessible, also works for the standard fine structural $L[\mathbb{E}]$ models $M$ for short extenders, for instance if $M$ has no largest cardinal, and assuming $M$ has Mitchell-Steel indexing, though I expect it would also work with Jensen indexing. So if those models are indeed consistent through ZFC + superstrongs, then one would need more than ZFC + ``There is a superstrong extender'' to prove there is a non-inaccessible $\alpha$ with $V\_\alpha$ modelling $\mathfrak{ZFC}(\mathsf{SOL})$.


(The paper "The definability of the extender sequence $\mathbb{E}$ from $\mathbb{E}\upharpoonright\aleph\_1$ in $L[\mathbb{E}]$" contains enough to generalize the argument of Kennedy, Magidor, Väänänen for $L$. The definability there is all done over $\mathcal{H}\_\kappa$s, as it's more convenient, but that can be translated into the cumulative hierarchy with the usual coding; in the present case that's only actually needed at the very top, since we can assume $V\_\alpha\models\mathrm{ZFC}$ to start with.)


Edit 3: Following @AsafKaragila's suggestions in the comments, we have:


Claim: Suppose $V\_\lambda$ models $\mathfrak{ZFC}(\mathsf{SOL})$ but $\lambda$ is singular. Then for every $X\in V\_\lambda$, $X^\#$ exists. Moreover, there is a proper class inner model $M$ with a measurable cardinal.


Proof: For simplicity take $X=\emptyset$. Suppose first that $0^\#$ does not exist. Note first that since $V\_\lambda$ models ZFC, $\lambda$ is a (singular) strong limit cardinal. By Jensen's covering lemma, $\lambda$ is singular in $L$. Let $B$ be the constructibly least singularization. Then $B$ can be defined over $V\_{\lambda+1}$ (without parameters), which contradicts $\mathfrak{ZFC}(\mathsf{SOL})$.


The argument for an inner model $M$ with a measurable is likewise, but using the Dodd-Jensen core model: We also have the appropriate version of covering for that core model $K=K^{\mathrm{DJ}}$, and $K|(\lambda^+)^K$ can also be defined in the codes over $V\_{\lambda+1}$, and hence the least singularization of $\lambda$ in the $K$-order is definable.


So Edits 1 and 3 together give that ZFC + "There is a singular $\lambda$ such that $V\_\lambda\models\mathfrak{ZFC}(\mathsf{SOL})$" is equiconsistent with ZFC + "There is a measurable cardinal".


