Is any true sentence in the second-order Peano Axioms provable Forgive the elementary nature of the question. I understand that the second order Peano Axioms are categorical in the sense that all their models are isomorphic. This equivalence class of models is taken to be the definition of natural numbers. 
My question is that: Is the theory defined by those second order axioms complete? i.e. is every second-order statement in this theory provable or disprovable from the axioms?
For the first order Peano Arithmetic axioms any statement that is true in all models is provable or disprovable by the completeness of first-order logic, but of course this is in applicable to the second-order axioms.
 A: Note that there are two different types of models of second-order logic: standard models, where second-order quantified variables range over all subsets of the domain; and Henkin models, where second-order quantified variables are allowed to range over a proper subset of the full power-set.
Henkin proved the completeness theorem for second-order logic for Henkin models, so if a sentence is true in all Henkin models, it is derivable. For completeness to hold, it is not enough to consider only standard models, so even though second-order PA is categorical for standard models, it is not complete (as we would expect, this being a corollary Gödel's theorem).
A: Between them, the previous comments and replies have already covered all of the relevant points, but here in any case is a direct, unsophisticated answer:
Any effective procedure (i.e. anything you could program up) for proving statements of second-order logic must be incomplete (unless it proves false statements). Otherwise, because second-order arithmetic is categorical, we would have an effective procedure for determining the arithmetic truth. But this is impossible by Gödel's first incompleteness theorem.
A: If a theory has only one model, then of course it is complete, in the sense that any 
statement or its negation is a consequence of the theory, because either it holds in the unique model or it doesn't. 
As you mention, there is only one model of second-order PA, and this is the model of the natural numbers. Thus, second-order PA is complete for first order assertions. 
One can easily extend this to second-order assertions by observing that any isomorphism of the first-order structures will extend to an isomorphism of the second order structures also, if one decrees that the second-order part of the structures should contain all subsets. Thus, there is up to isomorphism only one second-order structure of second-order PA, and so the theory is complete for second-order assertions. 
BUT, there are interesting things still to say about incompleteness. And the reason is that the concept of second-order is a set-theoretic concept, and so the question of which statements are true in this unique second-order model of second-order PA will exhibit many set-theoretic independences. That is, ZFC proves that the theory of the natural numbers is a complete theory, but different models of ZFC will have their natural numbers satisfying different statements. This is true already in the first order theory, since some models of ZFC will have the arithmetic statement Con(ZFC) being true in their natural numbers, but others will have the negation of this being true in their natural numbers. 
Because of this kind of issue, many logicians prefer to understand the second-order theory in a first-order way, by saying that one specifies a second-order model by giving first it's first order part, and then also specifying the collection of subsets that are to be used as the interpretation of the second-order part. Thus, a second-order model of PA consists of a first order structure (N,+,.,<,0,1) together with a collection S of subsets of N, to be used for interpreting the second-order quantifiers over subsets. In this weaker sense of second-order, one loses the categoricity, and there can be non-standard models again even in the first-order part.
