Why is ZFC incapable of interpreting second-order logic?
Also, when we say this, are we talking about ZFC as a background theory or using ZFC in some different way?
I am interested in this answer from Asaf Karagila, which says the following. I replaced a footnote with a comment in parentheses.
The point is that using ZFC we can interpret (in the non-technical
sense) second-order logic. ZFC gives us a way to understand the notion
of sets and relations which are necessary for second-order logic.
The following comment by Noah Schweber further clarifies that ZFC does not interpret second-order logic in a technical sense.
This is obviously right, but I tentatively think the word "interpret" in the first sentence might better be replaced with something else since when we use its technical meaning that's false.
I'm curious why this is the case.
If we assume ZFC in the background, though, as is routinely done, then we have a straightforward way to talk about the truth conditions of a second-order quantifier.
Let $2^D$ be the real (i.e. according to ZFC) powerset.
$$ M, v \models \forall x : \mathrm{Pred}[D] \mathop. \varphi(x) \;\;\textit{if and only if}\;\; M, v \models \varphi(w) \; \text{for all $w$ in $2^D$} $$
We can similarly talk about the truth conditions of function variables and higher-order functions and predicates.
Best Answer
The word "interpret" is usually used to compare two theories (or structures) in the same logic, so I'm going to avoid using it entirely here. Also, for simplicity I'll adopt a Platonist perspective here and assume that we're living in some "true" mathematical universe with a "true" second-order-logic satisfaction relation $\models_2$.
Every $\omega$-model $\mathcal{M}$ of $\mathsf{ZFC}$ (for simplicity, let's ignore non-$\omega$-models, although they don't really change things very much) has a version "$\models_2^\mathcal{M}$" of the satisfaction predicate for second-order logic. There are two ways that this predicate differs from $\models_2$:
It's only applicable to structures inside $\mathcal{M}$. It makes no sense to ask whether $\mathcal{A}\models_2^\mathcal{M}\varphi$ for $\mathcal{A}\not\in\mathcal{M}$.
More significantly, even when $\mathcal{A}\in\mathcal{M}$, the predicate "$\mathcal{A}\models^\mathcal{M}_2$" is determined via reference to what $\mathcal{M}$ thinks is the powerset of $\mathcal{A}$.
This second bulletpoint is absolutely lethal. For example, there is a second-order sentence $\theta$ such that $\theta$ is ("truly") true in exactly the uncountable structures. By downward Lowenheim-Skolem, there is a countable $\omega$-\model $\mathcal{M}\models\mathsf{ZFC}$. We then have for example $$\mathbb{R}^\mathcal{M}\models^\mathcal{M}_2\neg\theta\quad\mbox{but}\quad\mathbb{R}^\mathcal{M}\models_2\theta.$$ In general, the version of second-order logic developed inside an $\omega$-model of $\mathsf{ZFC}$ may "get lots of stuff wrong." This is in contrast to first-order logic, which is appropriately absolute. Note that this is really about first-order logic, not $\mathsf{ZFC}$ specifically - passing to a stronger theory will not help at all.
There are many more observations. For example, the set $\mathit{Taut}_2^\mathsf{ZFC}$ of "$\mathsf{ZFC}$-provable second-order tautologies" $$\mathit{Taut}_2^\mathsf{ZFC}=\{\varphi\in\mathsf{SOL}:\mathsf{ZFC}\vdash\forall \mathcal{A}, \mathcal{A}\models_2\varphi\}$$ is computably enumerable. But the set of actual second-order tautologies is not c.e. ... and $\mathsf{ZFC}$ can prove that!
Of course it is consistent (assuming mild hypotheses) that there is an $\omega$-model $\mathcal{X}$ of $\mathsf{ZFC}$ which "computes second-order satisfaction correctly," in the sense that $\models_2^\mathcal{X}$ coincides with $\models_2$ on all structures in $\mathcal{X}$: if $V_\kappa\models\mathsf{ZFC}$ then obviously $V_\kappa$ has this property! But this doesn't make up for the above issues. Also, we might want more - e.g. that $\mathcal{X}$ computes $\mathit{Taut}_2$ correctly - and then things get massively more difficult: for example, if there is a measurable cardinal then we have $$\mathit{Taut}_2^{V_\kappa}=\mathit{Taut}_2\implies\kappa\mbox{ is greater than the least measurable cardinal},$$ and so on.
I've avoided talking about non-$\omega$-models since they really just make things weirder, and we already see the core issue emerge with $\omega$-models. For example, if $\mathcal{M}$ is a non-$\omega$-model of $\mathsf{ZFC}$, then $\models_2^\mathcal{M}$ differs from $\models_2$ in a third way: we will have things $\mathcal{M}$ thinks are second-order sentences which are not actually finite. (This even trickles down to the first-order side of things, where the absoluteness of first-order logic referred to above breaks down when we look at nonstandard sentences - see Hamkins/Yang, Satisfaction is not absolute, which explains the importance of the adverb "appropriately" a couple paragraphs above.)