Incompleteness theorems for theories with omega-rule

If $T$ is a recursively axiomatized theory of second-order arithmetic (or set theory) that extends, say, $\mathrm{ACA}_0$, you can define a well-behaved provability predicate $\Pr^\omega_T(x)$ expressing provability in $T^\omega$ (i.e., $T$ extended with the $\omega$-rule) by a $\Pi^1_1$ formula. It is then not particularly difficult to check in $T^\omega$ that this predicate obeys the usual Hilbert–Bernays–Löb derivability conditions, and therefore $T^\omega$ is subject to Gödel’s second incompleteness theorem (and Löb’s theorem): if $T^\omega$ is consistent, then $T^\omega\nvdash\neg\Pr^\omega_T(\bot)$. See Boolos, The Logic of Provability.

Footnote to Emil Jeřábek's answer:

(1) Rosser (Journal of Symbolic Logic, 1937) was the first to show that there is a true $\Sigma^1_1$-statement that is unprovable in (second order arithmetic + the $\omega$-rule) with the essentially the same proof outlined by Emil.

(2) In contrast, as shown in a 1961-paper of Grzegorczyk, Mostowski, and Ryll-Nardzewski, every true $\Pi^1_1$-statement is provable in (second order arithmetic + the $\omega$-rule).

I learned the above facts as a graduate student from Barwise' article "The role of the Omitting Types Theorem in infinitary logic" (see p.57), published in Arch. math. Logik 21 (1981),55-68.