Analogues of worldly cardinals for (an unusual version of) second-order $\mathsf{ZFC}$ 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.
Building off of this MSE question of mine, 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.
 A: 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".
A: As discussed in the comment, Theorem 8.5 in the paper Inner Models from Extended Logics: Part 1 by Kennedy, Magidor, and Väänänen gives a consistent answer that, assuming $V=L$, models of $\mathfrak{ZFC}(\mathsf{SOL})$ are exactly those isomorphic to models of $\mathsf{ZFC}$ of the form $L_\kappa$ where $\kappa$ is inaccessible.
