One of the features of first order logic is that the provability relation is recursively enumerable: given any recursive first order theory, there is a Turing m

One of the features of first order logic is that the provability relation is recursively enumerable: given any recursive first order theory, there is a Turing machine that can list every theorem of that theory (although of course it will run forever). Additionally, first order logic is complete: for every statement true in all models of a theory, there is a proof of the statement from the theory. These two constraints cannot both be satisfied in a sound deductive system for second order logic. To see that this is so, consider that in second order logic we can prove Dedekind's categoricity theorem: there is only one model (up to isomorphism) of the second order Peano axioms (PA2). Let's assume that the provability relation for second order logic is recursively enumerable. We know from Gödel's incompleteness theorem that the set of first order sentences true of the natural numbers is not recursively enumerable. So take a sentence of the form "If PA2 then _" for some sentence _ which is in that set but not in the extension of the provability relation (this is a legitimate statement since the PA2 axioms are finite so we can just take their conjunction). This should be a logical truth of second order logic, but it's not provable (by the argument just given), so second order logic is incomplete: there are statements which are logical consequences yet are unprovable. So in other words, yes, the incompleteness theorem is very much at play in this limitation of second order logic. For the technical details I very much recommend chapters 3 and 4 of Shapiro's book; it's not terribly expensive, and any decent university library should have a copy. (A small footnote to my earlier post: Shapiro's book originally came out in 1991, not 2000—that's just the date of the paperback edition, and I'm unsure as to whether there are any substantial differences between the two.)