are there non-standard models of arithmetic in second order arithmetic?

Let $\mathsf{PA_2}$ be a standard recursively axiomatized second-order Peano Arithmetic (e.g. the theory which Hilbert and Bernays call $\mathsf{Z}_2$). And interpret the wffs of $\mathsf{PA_2}$'s language with the 'full' semantics, where the second-order quantifiers are constrained to run over the full collection of sets of numbers.

Then (i) Gödel's theorem applies, of course, to $\mathsf{PA_2}$, so (assuming consistency) there will be a true canonical Gödel sentence $\mathsf{G}$ such that $\mathsf{PA_2} \nvdash \mathsf{G}$.

However, (ii) $\mathsf{PA_2}$, with the full semantics, is categorical by Dedekind's argument, so has only one model (up to isomorphism). In that one model, $\mathsf{G}$ is true, so $\mathsf{PA_2} \vDash \mathsf{G}$.

This shows that syntactic provability $\vdash$ falls short of semantic entailment $\vDash$ in the scecond-order case (there is no complete deductive system for second-order consequence, assuming the full semantics).

In summary, then, while the claim "$\mathsf{PA}$ settles all arithmetical truths" is false however we interpret it (where $\mathsf{PA}$ is first-order Peano Arithmetic), the situation with the corresponding claim "$\mathsf{PA_{2}}$ settles all arithmetical truths" is more complex. It depends whether you mean "semantically entails" or "deductively implies".

For vividness, it may well help to put that symbolically. We'll use $\{\mathsf{PA}, \vdash\}$ to denote the set of theorems that follow in $\mathsf{PA}$'s formal proof system, and $\{\mathsf{PA}, \vDash\}$ to mean the set of sentences semantically entailed by $\mathsf{PA}$'s axioms (given the standard semantics for first-order arithmetic). Similarly, we'll use $\{\mathsf{PA_{2}}, \vdash_2\}$ to mean the set of theorems that follow in $\mathsf{PA_{2}}$'s formal proof system, and $\{\mathsf{PA_{2}}, \vDash_{2}\}$ to mean the set of sentences semantically entailed by $\mathsf{PA_{2}}$'s axioms (given the "full" semantics for the quantifiers). Finally we'll use $\mathcal{T}_{A}$ to denote the set of truths of first order arithmetic (often called, simply, True Arithmetic); and we'll now use $\mathcal{T}_{2A}$, the set of truths of the language of second-order arithmetic (True Second-Order Arithmetic). Then we can very perspicuously display the relations between these sets as follows, using `$\subset$' to indicate strict containment:

$\{\mathsf{PA}, \vdash\} \;=\; \{\mathsf{PA}, \vDash\} \;\subset\; \mathcal{T}_{A}$

$\{\mathsf{PA_{2}}, \vdash_2\} \;\subset\; \{\mathsf{PA_{2}}, \vDash_{2}\} \;=\; \mathcal{T}_{2A}$.

The completeness of first-order logic which yields $\{\mathsf{PA}, \vdash\} = \{\mathsf{PA}, \vDash\}$ is, though so familiar, a remarkable mathematical fact which is enormously useful in understanding $\mathsf{PA}$ and its models. This has led some people to think the strict containment $\{\mathsf{PA_{2}}, \vdash_2\} \subset \{\mathsf{PA_{2}}, \vDash_{2}\}$ is a sufficient reason to be unhappy with second-order logic. Others think that the categoricity of theories like second-order arithmetic, and the second-order definability of key mathematical notions like finiteness, suffices to make second-order logic the natural logic for mathematics. Stewart Shapiro's Foundations without Foundationalism is a classic defence of the second position.

The issue here is discussed at some length in Ch. 29 (or Ch. 22 of the 1st edition) of my Gödel book, if you want more!

The distinction between "first-order semantics" and "full second-order semantics" for arithmetic is somewhat muddy in much of the literature, and the overuse of the terms "first-order" and "second-order" to mean many different things only confuses the issue more (the same is true for "completeness").

In plain terms, the only difference between formalizing arithmetic in first-order semantics and formalizing it in full second-order semantics is that in the former case we look at all models (in the usual sense) for the theory, while in the latter case we only look at the standard model. This is not the way full second-order semantics is usually defined, but when we combine the usual definition with the well-known categoricity results, we see that this restriction is exactly the effect of full second-order semantics for arithmetic.

But nothing else changes. The syntax and the deductive systems for "second-order arithmetic" are exactly the same regardless of which semantics is used. Because the incompleteness theorems are proved syntactically, they continue to apply in their syntactical sense regardless of which semantics we use.

What does change is that the completeness theorem fails when we move to full second-order semantics, because we have excluded by fiat many of the models required for every syntactically consistent theory to have a model. Thus the semantic consequences of the incompleteness theorems, such as the existence of nonstandard models, do not go through in full second-order semantics, because we have already eliminated all nonstandard models from discussion. This is a side effect of full second-order semantics - because the completeness theorem fails, it becomes necessary to carefully distinguish between syntactic and semantic definitions for concepts such as (logical) implication and consistency.

When we use first-order semantics for second-order arithmetic, which is what is typically done in the literature these days, there are indeed many nonstandard models. These models vary from the standard model in two ways. First, the set of "numbers" may be different from the standard set of natural numbers. Second, the collection of "sets of numbers" may be a proper subcollection of the true powerset of the set of "numbers". There are many of these nonstandard models, and we know quite a bit about their properties from research in the field of Reverse Mathematics.

The fact that moving to full second-order semantics is no different than just working with the standard model is one reason that these semantics are not so useful. Anything we could do with full second-order semantics, we could do in our usual first-order semantics by just talking about the standard model explicitly. Any question that we cannot answer about the standard model when working in ZFC will be equally unanswerable when we work with full second-order semantics.

In Second Order Logic , PA2+not (G), where G is the first sentence of GÖdel, is consistent. But we know that G is true in the standard model and the unique model of PA2 is the standard model. What is the solution to this? PA2+not (G) is consistent, you never prove a contradiction from it, but it has no model. In second order a theory can be sintacticaully consistent, but have no models. In first order it don´t matter. If a sentence S is undecidable in a first order theory T1, you have 2 models ( at lest) for it, it is said: if theory T1 is consistent , like is in first order it has a model, and T1+S and T1+ not(S) will be consistent both of them, everyone with his models