Incompleteness theorems for theories with omega-rule Recall that the omega-rule is an infinitary rule of inference that allows one to deduce $\forall x A(x)$ from $A(0), A(1), \dots$. It's known that adjoining PA (or even Q) with the omega-rule results in a complete theory (true arithmetic). I'm curious what happens to stronger theories when we allow the omega-rule as the sole infinitary rule of inference (and all the axioms must be recursively enumerable, as I will hereafter assume). For example, can there be a complete theory of analysis or set theory if we allow ourselves the omega-rule? I suspect the answer is no, but I'm not sure how to prove it.
We can also generalize the omega-rule to allow deducing a universal statement from the set of all true instances of size at most, say, $2^{\aleph_0}$ (so for example, deduce $\forall x \in \mathbb{R} B(x)$ from the $2^{\aleph_0}$ instances of $B(x)$ for each real number $x$). Again, I suspect but cannot prove that there will be a sufficiently strong theory (something stronger than analysis) that must be incomplete even if one allows this generalized omega-rule (and similarly for generalized omega-rules for each cardinality).
 A: 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.
A: 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.
