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 A, either A 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?