(This question is the "leftover" part of this old question of Mallik, which was substantially clarified in the comments. Throughout, "second-order logic" refers to the standard semantics.)
Let $ZFC_2^{def}$ be the theory in second-order logic consisting of:
-
The usual (first-order) formulations of Infinity, Pairing, Union, Powerset, Extensionality, and Foundation.
-
The Separation and Replacement schemes for second-order formulas.
(The "def" here stands for "definite," see the original question linked above.) My question is:
Is it consistent that $ZFC_2^{def}$ has a countable model?
(A bit more precisely: is the first-order statement "$ZFC_2^{def}$ has a countable model" consistent with first-order ZFC? It's perfectly kosher to reason about second-order logic inside a first-order system.)
A couple comments:
-
It's crucial that we're using first-order Powerset instead of second-order Powerset here, since of course Infinity + second-order Powerset ensures uncountability. On the other hand, it's not hard to show that we could replace first-order Foundation with second-order Foundation without changing the theory: that is, all models of $ZFC_2^{def}$ are well-founded.
-
The Separation scheme for second-order formulas is not what's generally referred to as "second-order Separation:" the former is the scheme consisting of $$\forall \overline{a}\forall x\exists y\forall z(z\in y\leftrightarrow z\in x\wedge \varphi(\overline{a}, z))$$ for $\varphi$ a second-order formula, while the latter is the single axiom $$\forall x\forall A\exists y\forall z(z\in y\leftrightarrow z\in x\wedge z\in A).$$ Similarly, the Replacement scheme for second-order formulas is a priori weaker than the single axiom generally referred to as "second-order Replacement."
-
It's not hard to show that $ZFC_2^{def}$ consistently doesn't have a countable model (as my answer to Mallik's original question does) but this uses an additional set-theoretic assumption: that there is a nice well-ordering of enough of the universe.
Best Answer
Yes, it is possible that there are countable $ZFC_2^{def}$ models. We start with $V=L$ and an inaccessible cardinal $\kappa$. The model will be $M=V_\kappa^L$ in the forcing extension $L[G]$ where $G$ is $\operatorname{Col}(\omega,\kappa)$-generic over $L$. Of course the interesting axioms to check are the speraration and replacement schemes for 2nd order formulas. Lets do separation as it is notationally easier.
Assume $a, p\in M$ and that $\varphi(x, y, z)$ is a 2nd order $\in$-formula. Note that $$b=\{c\in a\mid (M, \mathcal P (M))\models \varphi(c, a, p)\}^{L[G]}$$ is ordinal definable in $L[G]$ since $M=V_\kappa^L$ (and thus $\mathcal P(M)$) is and $a, p$ are definable from there position in the canoncial wellorder of $L$. As $a\subseteq HOD^{L[G]}$ we have $b\in HOD^{L[G]}$. As is well known, $\operatorname{Col}(\omega, \kappa)$ is ordinal definable and cone homogeneous and thus $HOD^{L[G]}\subseteq HOD^L=L$ so that $b\in M$.
Replacement works similar, however there one needs to appeal to the regularity of $\kappa$ in $L$.