are there non-standard models of arithmetic in second order arithmetic? non-standard models of arithmetic in second order arithmetic?
Background:
According to Godel's theorem, if we have, in a given consistent system S, a non-provable wff. A, then we can extend the system to either S1 or S2 by including A or ~A as a new axiom, respectively. Both S1 and S2, according to Godel, will be consistent. If S is a first order system, then both S1 and S2 have at least a model, (let us call them M1 and M2) and the two models are essentially different because in M1 A is true, but in M2 ~A is true.
If S is PA (peano arithmetic), then that means that there are infinitely many unintended models in addition to the natural numbers, each one obtained by extending PA with a new axiom which is not true for the model of the natural numbers. These unintended interpretations are named non-standard models of arithmetic. 
The question(s):
The above conclusions refer to first order systems. However, it is unclear to why this argument is restricted to first order systems, as Godel's proof is also valid for second order systems: Any extension of second order PA can be consistently extended into two different systems by including any non-provable wff. A or ~A as a new axiom, respectively. These two systems should in turn describe two essentially different models, and so there should also be non-standard models of arithmetic in second order arithmetic.
The problem is, that it is often stated that second order PA determine the set of natural numbers uniquely, and so there should be not room for non-standard models of arithmetic in second order arithmetic, which contradicts what . 
Metaquestion: I am sure there is something wrong in my reasoning leading to this contradiction. But I cannot find any errors, can anybody help me, please!!!!
 A: This is a late answer, but I think I can condense the answers in a short form.

The incompleteness theorem states that there is a neither provable nor disprovable sentence $\varphi$. This can have two reasons:


*

*$\varphi$ is neither true nor false in the general case, i.e. there are models in which $\varphi$ is valid and models in which it is not.

*$\varphi$ is true or false in general, but we cannot deduce $\varphi$ or $\neg\varphi$ because there is something wrong with our deductive system.


The completeness theorem for first-order logic excludes option 2. For second-order theories with a single model we can exclude option 1. We are left with the other option respectively.
A: 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
A: 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!
A: 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. 
