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



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*.


