Is there a result for second-order theories analogous to Gödel's second incompleteness theorem?

Question

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

Answer 1

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.