I know that the natural numbers can be categorically characterized in second-order logic with the standard semantics. However, I could not find an example of a non-standard Henkin structure (one that is closed under parametric definability) that is a model for these characterizing axioms. Is there a known example of such structure?
Thanks!
Well, there aren't really explicit examples, basically because of Tennenbaum's Theorem. But they exist, via the Compactness Theorem for first-order(!) logic.
Specifically, consider the two-sorted, first-order structure $(\mathbb{N}, \mathcal{P}(\mathbb{N}); +, \times, 0, 1, \in)$. It has a theory, $T$; by compactness, the theory $T\cup\{c>\underline{n}: n\in\mathbb{N}\}$ has a model, where $c$ is a new constant symbol and $\underline{n}$ is the usual term denoting $n$ (sometimes called a numeral). Any model of $T$ is a two-sorted, first-order structure of the form $$(\mathcal{N}, \mathcal{S}; +, \times, 0, 1, \in, c).$$ Forget the $c$; the reduct $(\mathcal{N}, \mathcal{S}; +, \times, 0, 1, \in)$, viewed as a Henkin model, has the properties you desire.
For example, we can fix a nonprincipal ultrafilter $\mathcal{U}$ on $\mathbb{N}$, and look at the ultrapower of $\prod (\mathcal{N}, \mathcal{S}; +, \times, 0, 1, \in)/\mathcal{U}.$ This will be a Henkin model of second-order PA.
The point is that Henkin semantics is just first-order logic in disguise; so all the arguments are basically the same.
Actually, what I've sketched above is rather overkill: any model of the (two-sorted, first-order) theory $Z_2$ can be viewed as a Henkin model of second-order $PA$. Then just take any nonstandard model of $Z_2$.
There are two ways for a Henkin model of second-order arithmetic to be nonstandard. 1: it could have a standard first-order part of $\omega$, but less than the full powerset of $\omega$ as its second order part. 2: it could have a nonstandard first-order part, in which case the second-order part must necessarily be nonstandard. The first kind of model is called a (nonstandard) $\omega$-model, while the second kind could be called $\omega$-nonstandard. Models of both of these kinds are very commonly studied in mathematical logic.
Nonstandard $\omega$-models are easy to construct. For example, let $A$ be the collection of subsets of $\omega$ that are definable in the language of second-order arithmetic, without parameters. Then $(\omega, A, \ldots)$ is a model of second-order arithmetic $\text{Z}_2$. A set that is definable relative to definable parameters is definable without parameters, so the model is closed under definability. Another example, assuming $V \not = L$ at the level of $P(\omega)$, would be a structure of the form $(\omega, P(\omega) \cap L,\ldots)$.
$\omega$-nonstandard models are harder to construct because not every model of first-order arithmetic is the first-order part of a model of second-order arithmetic $\text{Z}_2$. For example, if we have a model of $\text{PA} + \lnot\text{Con}(\text{PA})$ then this cannot be the first-order part of a model of $\text{Z}_2$ because $\text{Z}_2$ proves $\text{Con}(\text{PA})$.
On the other hand, because ZFC proves that $(\omega, P(\omega), \ldots)$ is a model of $\text{Z}_2$, if we take any $\omega$-nonstandard model of ZFC, and consider just its second-order part, that will be an $\omega$-nonstandard model of $\text{Z}_2$.
Another way to obtain an $\omega$-nonstandard model of $\text{Z}_2$ is to build the first- and second-order parts at the same time, by applying the compactness theorem directly to the theory $\text{Z}_2$, in the same way that nonstandard models of PA are constructed.
