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 $ACA_0$ can be viewed as a Henkin model of second-order $PA$. Then just take any nonstandard model of $ACA_0$.

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

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)$ 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 $ACA_0$ can be viewed as a Henkin model of second-order $PA$. Then just take any nonstandard model of $ACA_0$.

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 $ACA_0$ can be viewed as a Henkin model of second-order $PA$. Then just take any nonstandard model of $ACA_0$.