(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.

  • $\begingroup$ In your last comment, $ZFC_2^{def}$ should replace $T$, right? $\endgroup$
    – Z. A. K.
    Feb 17, 2020 at 19:30
  • $\begingroup$ @Z.A.K. Yup, fixed. $\endgroup$ Feb 17, 2020 at 19:30
  • $\begingroup$ Now when you say kosher, what exactly do you mean? Who was the rabbi overseeing the process? From which Jewish tradition he came? What is his approach to modernity? $\endgroup$
    – Asaf Karagila
    Feb 18, 2020 at 9:51

1 Answer 1


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$.

  • 1
    $\begingroup$ Nice, +1! (FWIW it may be simpler to just say $M=L_\kappa$.) At a glance this looks right, I'll accept when I've had a few minutes to read it properly. $\endgroup$ Feb 19, 2020 at 18:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .