It is important to distinguish the "complete" which is in Gödel's completeness theorem and the "complete"-s in the incompleteness theorems, because these are not the same.
The first one presupposes two things, a) a syntax for a logical language, also containing a syntax for proofs b) a notion of model. Then, a combination of a) and b) is complete if every sentence which holds in all models is also syntactically provable.
The second one for our purpose can be summarized as follows: a syntax for a logical language is complete if for every sentence , either or its negation is provable. This sense of completeness does not mention models or semantics!
The main point in Gödel's first incompleteness theorem is the ability to internally represent the syntax and proof theory of the language. In the case of first-order PA, all syntactic objects appear as certain finitely deep and finitely branching trees, and the job is to use arithmetic operations and properties to encode various finitary trees as just unary branching trees, i.e. the natural numbers. The syntax of second-order arithmetic does not differ in a relevant way; it is also just finitary trees, and since second-order arithmetic is a strict extension of first-order arithmetic, analogous internal encoding works in it as well.
That second-order logic "doesn't have a computable deduction system" sounds false to me. It certainly does not have the completeness property (in the first sense) with respect to the standard notion of model, precisely because of Gödel's incompleteness + ruling out nonstandard semantic natural numbers. But second-order logic still has finitary, recursively enumerable syntax and proofs, with decidable proof validation.
I see. So the answer is that it is indeed true that Godel's statement is true in all models of second-order PA, but unprovable nonetheless since Godel's completeness theorem isn't true for second-order logic?
Second order logic can also arithmatise sentences, and also has fixed points. So the usual proofs carry over about the 1st incompleteness theorem. But there's an easier way to see this. There can't be any computable procedure to check if a second order sentence is valid or not, because if there was we could check if PA->Theorem and therefore decide Peano Arithmetic and therefore the Halting problem.
I'm following the HAE sequence [Godel's Completeness and Incompleteness Theorem], and I can see what it means for first-order logic to be incomplete.
I don't understand how Godel's incompleteness theorem can still apply to second-order logic -- doesn't PA with second-order logic allow us to uniquely pin down a model?
But Godel's sentence can still be constructed, so second-order logic must still be incomplete -- I just don't understand how we can have models with a "weird idea of what it means to be a proof" if we don't have non-standard numbers.
I asked on Math Stackexchange and was told that second-order logic "doesn't have a computable deduction system". Unfortunately, I don't really understand what this means.