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)$."