Is there a result for second-order theories analogous to Gödel's second incompleteness theorem? One formulation of Gödel's second theorem says that, if $T$ is a consistent, axiomatisable extension of $PA$, and  then $T$ cannot prove $\neg Prv(\ulcorner 0=1 \urcorner)$, where $Prv(-)$ is a predicate in the language of $T$ satisfying the Hilbert-Bernays derivability conditions. By my understanding, what this means is that if a first-order theory is capable of encoding its own syntax, and if it has a predicate satisfying the Hilbert-Bernays derivability conditions, then it can encode a statement that it is provably consistent, but that statement is undecidable.
I have two questions. 
1) Is my understanding of the theorem correct? In particular, I want to know whether I am making a mistake by dropping reference to extensions of $PA$.
2) Is there an analogous result for second-order theories? Something like, "for $T$ in such-and-such class of consistent second-order theories, $T$ cannot prove $\neg Prv(\ulcorner \neg Con(T) \urcorner)$."

In Gödel's original paper (1931), see : Jean van Heijenoort (editor), From Frege to Gödel : A Source Book in Mathematical Logic (1967), page 592-on, the results was proved for the following system : 

If to the Peano axioms we add the logic of Principia Mathematica (with the 
  natural numbers as the individuals) together with the axiom of choice (for all types), we obtain a formal system $S$, for which the following theorems hold [...].

And see page 600 for the induction axiom (and not axiom schema).
Thus, Gödel's reuslts apply to second-order theories.

But you have to take into account that second-order logic itself is "incomplete" in the sense of Gödel's Completeness Theorem.
