Incompleteness of Second-order PA I'm trying to reconcile Godel's Incompleteness Theorem with the fact that $\mathbb{N}$ is the canonical model of second-order PA. If there is a statement $S$ that is undecidable in PA, then it would seem that PA + S and PA + $\lnot S$ are both consistent models of Peano Arithmetic, contradicting the uniqueness of $\mathbb{N}$. What am I missing here?
A related question is the notion of "true but unprovable": what is the basis for saying that an unprovable statement in arithmetic is true, when it can't be proven from the axioms?
 A: You ask about things that are "true but unprovable". This does indeed sound paradoxical: if I say that $\alpha$ is true but unprovable, presumably I have proved that $\alpha$ is true - so what gives?
The issue is that when we say something like that, we're hiding details. Specifically, whenever someone says "provable," they mean "provable from some axioms". You'll often hear Goedel's incompleteness theorem stated as "There is a true but unprovable sentence." This is a vast, and misleading, simplification. Here's the right way to phrase it:

$(*)\quad$ Suppose $X$ is a set of sentences in the language of arithmetic which isn't too complicated (technically: is recursively enumerable) and contains all the axioms of first-order PA. Then there is a sentence $\varphi$ such that - if $X$ is consistent - $\varphi$ is true and not provable from $X$.

$(*)$ is provable in PA, incidentally. By the way, "PA" can be replaced throughout with much much weaker systems, but I'm not going to focus on that here. Also, a historical note: $(*)$ is actually Rosser's improvement of Goedel's original theorem.
Note that $\varphi$ depends on $X$! There isn't a single $\varphi$ which is "true but unprovable" in some universal sense; rather, each (consistent, recursively enumerable) theory $X$ yields its own $\varphi$. 
Moreover, the proof that $\varphi$ is true takes place not in $X$, but rather in the theory PA+"$X$ is consistent" (note the hypothesis that $X$ be consistent in the statement above). So - as long as $X$ is consistent! - $\varphi$ is true, but the only way we know that $\varphi$ is true is by accepting PA+"$X$ is consistent", and this goes beyond what $X$ itself can do.

Incidentally, how does this interact with second-order PA? Well, the issue is that second-order logic is terrible: it has no complete proof system (and that's just scratching the surface). From a collection $X$ of first-order sentences, I can effectively enumerate the things $X$ proves - just search through all possible proofs! Since second-order logic doesn't have a complete proof system, though, that's not a possibility. So it doesn't really make sense to speak of something being "provable" from a collection of second-order sentences, at least not in the way we're used to thinking about proofs.
We could try to do the following: take $X$ to be the set of first-order consequences of second-order PA. The problem, now, is that this $X$ is not recursively enumerable, so Goedel's theorem doesn't apply to it.
A: Godel's Incompleteness Theorem is about first-order PA.  The usual natural numbers $\mathbb{N}$ is the unique (up to isomorphism) model for second-order PA, but no set of first-order axioms can produce a unique model unless that model is finite (which $\mathbb{N}$ isn't).
