Is second-order logic *with standard semantics* necessary to categorically characterise the natural number structure?

Question

Is second-order logic with standard semantics necessary to categorically characterise the natural number structure?

One can prove that any two models of Dedekind-Peano arithmetic are isomorphic (categoricity theorem), and, by invoking the isomorphism theorem, that one model of Dedekind-Peano arithmetic satisfies A iff any other model of Dedekind-Peano arithmetic satisfies A, for any sentence A (which gives us elementary equivalence).

My question: can one do the same with second-order logic and Henkin semantics or does one require standard semantics for this categoricity result?

I suspect that because Henkin semantics is almost the same as many-sorted first-order semantics, one cannot categorically characterise the natural numbers using Henkin semantics.

Answer 1

As you suspect, you cannot do this.

Here's one general fact which in particular kills this question (which is just an instance compactness for Henkin semantics): suppose $\Sigma$ is any language and $T$ is any second-order $\Sigma$-theory which has some infinite Henkin model. Then $T$ has Henkin models of arbitrarily large cardinality. This ultimately leans, just as you say, on the fact that Henkin semantics is really just two-sorted first-order logic plus some base axioms.

---

To clarify: by "Henkin model of $T$" I mean a pair $(S, P)$ where $S$ is a $\Sigma$-structure, $P=(P_i)_{i\in\mathbb{N}}$ is a family of relations on $S$, and $(S,P)\models T$ in the sense of Henkin semantics (in particular, every parameter-definable relation on $S$ is an element of $P$ - here "parameter" refers to both elements of $S$ and of $P$).

Indeed, the only point at which many-sorted first-order logic (which is what Henkin semantics second-order logic is an instance of) becomes genuinely different from first-order logic is when we have infinitely many sorts in play: the existence of an element not belonging to any sort is forbidden in the many-sorted context, but is allowed when we translate to the first-order context (by replacing sorts with unary predicates).