Below, the standard semantics of second-order logic is used.
My question is about a second-order analogue of $ZFC$ other than the usual "second-order $ZFC$." Rather than define the latter, I'll just state that its (set-sized) models are exactly the $V_\kappa$s with $\kappa$ strongly inaccessible (or if you prefer, the uncountable Grothendieck universes).
Specifically, I'm interested in the second-order theory consisting of the usual (first-order) axioms of Pairing, Extensionality, Union, Choice, Infinity, and Powerset, and the Separation and Replacement schemes ranging over second-order formulas. I'll call this "$ZFC_2^{scheme}$."
- Specifically, for each formula $\varphi(x, y_1,…,y_k)$ of second-order logic with only the displayed variables, each of which is first-order, we have a corresponding Separation and Replacement instance. We do not allow second-order parameters here, so formulas with second-order free variables don't yield Separation/Replacement instances.
The passage from $ZFC$ to $ZFC_2^{scheme}$ has a nice uniformity: it's an example of a more general operation $\mathcal{ZFC}$ which spits out a $ZFC$-analogue given a logic at least as strong as first-order logic.
- This is the reason for the parameter restriction above: I want $ZFC_2^{scheme}$ to look just like $\mathcal{ZFC}(\mathcal{L})$ for any other logic $\mathcal{L}$, and not take into account the particular feature that we now have a new kind of variable at our disposal – and in particular, take as "syntax-free" an approach to logics as we can get away with. (This is a choice of arguable value, but it's the one I'm making for now.)
It's easy to show that every model of $ZFC_2^{scheme}$ is well-founded, so to understand its models we only need to look at transitive sets. A natural hope at this point is that $ZFC_2^{scheme}$ is just second-order $ZFC$ in disguise, that is, that for a transitive set $M$ we have $M\models ZFC_2^{scheme}$ iff $M=V_\kappa$ for some strongly inaccessible $\kappa$. However, this isn't at all obvious to me (although it is easy to show the right-to-left direction).
Question. What are the (set-sized) models of $ZFC_2^{scheme}$?
(Note by contrast that the "arithmetic analogues" $PA_2^{scheme}$ and second-order $PA$ are equivalent since each pins down $\mathbb{N}$ up to isomorphism – although that leads to its own questions.)
(I'm happy to drop Choice if that would help.)
EDIT: As Hanul Jeon pointed out below, this answer shows that consistently $ZFC_2^{scheme}$ (there called "$ZFC_2^{def}$") has countable models, so we have a partial answer. However, I don't see at the moment a way to get an outright $ZFC$ proof that $ZFC_2^{scheme}$ is strictly weaker than second-order $ZFC$.
Best Answer
This is not a full answer to the question $``$What are the set-sized models of $ZFC^{scheme}_2?"$ however we will see that $ZFC^{scheme}_2$ is not significantly weaker than second order $ZFC$.
I claim that $ZFC$+$``$ there exists a model of $ZFC^{scheme}_2"$ is equiconsistent with $ZFC$+ an inaccessible (however, other than for second order $ZFC$, the existence of such a model does not outright imply the existence of an inaccessible).
So assume that $M$ is a transitive set-sized model of $ZFC^{scheme}_2$. We will show that $\delta=Ord\cap M$ is inaccessible in $L$. First lets see that $\delta$ is regular in $L$. The proof is very similar to the argument in your answer here. If not, then by basic properties of the $L$-hierachy there is a $\beta<(\delta^+)^L$ and a cofinal subset of $\delta$ of ordertype ${<}\delta$ in $L_\beta$. Since $\vert L_\beta\vert =\vert\delta\vert$, there is a binary relation on $\delta$ coding $L_\beta$. Thus $M$ can define the $L$-least singularising subset $A$ of $\delta$ by a $2$nd order formula (without $2$nd order parameters(!)) as follows:
\begin{align} \alpha\in A\Leftrightarrow&\exists E\subseteq Ord\times Ord\text{ such that }(Ord, E)\text{ is a wellfounded model of }V=L\\ &\text{ and there exists a map } \pi:Ord\rightarrow Ord\text{ such that } \pi(\gamma)\text{ is the $\gamma$-th ordinal}\\ &\text{ in } (Ord, E)\text{ and }\text{the least ordinal}\text{ of } (Ord, E)\text{ not in the range of }\pi\text{ is }\\&\text{ singular in }(Ord, E)\text{ and }\pi(\alpha)\text{ is in the least singularising subset according}\\&\text{ to the canonical wellorder }<_L\text{ of }(Ord, E) \end{align} A brief moment of reflection shows that this can indeed be expressed by a 2nd order formula and that it defines $A$. This clearly contradicts $M$ being a model of $ZFC^{scheme}_2$.
Lastly, $\delta$ cannot be a successor cardinal in $L$ since $L^M$ is the true $L_\delta$ and in that case, $M$ would have a maximal cardinal.