[Question] Godel in second-order logic?

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.

No comments.