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

  • $\begingroup$ Do Replacement and Separation of $ZFC_2^{scheme}$ allow second-order parameters? $\endgroup$
    – Hanul Jeon
    Mar 25, 2020 at 2:50
  • $\begingroup$ @HanulJeon Good point - no, they don't. I'll edit to add that. $\endgroup$ Mar 25, 2020 at 2:51
  • $\begingroup$ @HanulJeon Edited (thanks again). Let me know if I should clarify further. $\endgroup$ Mar 25, 2020 at 2:55
  • 2
    $\begingroup$ @CogitoErgoCogitoSum The question has already assumed the standard semantics, and second-order logic with standard semantics is not recursively axiomatizable. (Thus, nobody can present a full list of axioms of second-order logic.) $\endgroup$
    – Hanul Jeon
    Mar 25, 2020 at 8:32
  • 2
    $\begingroup$ @CogitoErgoCogitoSum This isn't about strengthening rigor, it's about comparing theories in different abstract logics (in the technical sense of abstract model theory). If you prefer, we can embed this whole question inside first-order ZFC ("Does ZFC prove that ...?") since the relevant definitions (specifically, the definition of second-order logic with the standard semantics) are expressible in the language of set theory. Put another way: nothing here is any more complicated, fundamentally, than "The set models of second-order $ZFC$ are exactly the strongly inaccessible levels of $V$." $\endgroup$ Mar 26, 2020 at 0:51

1 Answer 1


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.

  • $\begingroup$ Very nice! As you say this doesn't fully answer the question, but it's great to know that the gap between the two is provably not too strong (I'd initially had a guess like this but couldn't get the argument to work, so gave it up). $\endgroup$ Mar 26, 2020 at 0:49
  • $\begingroup$ I've decided to accept this since I now think that this question probably doesn't have a "clean" answer after all. $\endgroup$ Sep 17, 2020 at 22:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.