Categoricity of second order theories - precisely what does it mean?

The point is that you already assume there is some set theory in play when you talk about second-order logic.

In other words, you use first-order set theory to talk about second-order "everyday theories" like the natural numbers, etc.

Different models of $\sf ZFC$ can have wildly different sets which they regard as "the true $\Bbb N$". If $M$ is a model of $\sf ZFC$, then there are $M_0$ and $M_1$ which are elementary equivalent to $M$, but $M_0$ is countable, and therefore has only countably many "natural number objects", whereas $M_1$ is such that it has uncountably many "natural number objects". Certainly these are not isomorphic, even though the models themselves pretty much agree on "how things should look like".

So yeah, what we actually have is that first-order $\sf ZFC$ proves that the second-order theories of $\Bbb N$ etc. are categorical. Or, if you will, inside a fixed universe of set theory, $\Bbb N$ has a categorical second-order theory. But moving to a different universe might produce you with different theories and different models.


To supplement Asaf's answer, let me observe that there are natural second-order theories whose categoricity is undecidable in ZFC. Specifically, let's take second-order ZFC ("ZFC$_2$") itself!

It's easy to show in ZFC that any set-sized model of ZFC$_2$ (yes, models are required to be sets already, so this is redundant; but it's worth mentioning explicitly since we do sometimes care about class-sized "models," and when working with second-order logic is often such a time) is (up to isomorphism) of the form $(V_\alpha,\in)$ for $\alpha$ a strongly inaccessible cardinal. This tells us:

  • It is consistent with ZFC that ZFC$_2$ has no (set-sized) models. This nonexistence statement is just "There is no strongly inaccessible cardinal."

  • Now make the mild (hehe) assumption that ZFC + "There is exactly one inaccessible" and ZFC + "There are two inaccessibles" are each consistent (obviously the second implies the first, so this is a bit redundant, but what the hey). Then the former proves that ZFC$_2$ has a set-sized model and is in fact categorical, while the latter proves that ZFC$_2$ is not categorical.

The moral I'm trying to get at here is that second-order categoricity (and satisfiability) claims can't be made on their own; we really need a background universe of sets. Of course, every logic has some sort of set-ish commitment, but with second-order logic the overhead is just ridiculous.