Extra theorems of Peano Arithmetic with Omega Rule Are there any theorems that Peano Arithmetic with the infinitary inference rule "If $P(0)$, $P(S0)$, $P(SS0)$, $P(SSS0)$, etc all hold, then $\forall x P(x)$ holds" can prove, that regular Peano arithmetic can't? And can someone give me an example, if there is one.
 A: Sure - the consistency of (the usual version of) $PA$! (I'll write "$PA_\omega$" for "$PA$ plus the $\omega$-rule"; I believe this is standard.)
$Con(PA)$ is the statement "there is no proof of "$0=1$" from the axioms of $PA$;" when properly encoded (via Godel numbering), this is a statement of the form $\forall x\varphi(x)$, where $\varphi(x)$ involves only bounded quantifiers. The $\omega$-rule lets us prove all true $\Pi^0_1$ sentences, and so $Con(PA)$ is a "theorem" of $PA_\omega$.
There are other examples: for instance, if $p\in\mathbb{Z}[x]$ is a polynomial with no integer solutions, then $PA_\omega$ proves "$p$ has no integer solutions." By contrast, there are many such polynomials which $PA$ does not prove have no integer solutions! In fact, the question "Which polynomials have integer solutions?" is as complicated as it can be; this is the MRDP theorem due to Matiyasevitch, Robinson, Davis, and Putnam (see https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem).

In light of all this, we might ask the dual of your question:

Does $PA_\omega$ prove all true sentences in the language of arithmetic?

I'll leave this as an exercise. :)
