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.

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

• What's nice is that it starts to depend a lot on the meta-theory. If you work in a theory that proves $\operatorname{Con}\sf (ZFC)$, then $\sf PA_\omega$ will prove that, making it a nontrivlally strong theory. :-) – Asaf Karagila Jul 17 '15 at 20:41
• @AsafKaragila: I'm not sure I understand your comment. Why does it depend on the meta-theory at all? If Con(ZFC) is true in the naturals, then PA$_ω$ proves it, regardless of what meta-system we are using, as long as it is strong enough to prove the fact that PA$_ω$ proves every true $Π_1$-sentence. Right? We could just say that PA$_ω$ is so strong that it proves the consistency of every consistent theory. =) – user21820 Dec 13 '17 at 15:39
• @user21820: Uhh, if your meta theory is one where $\lnot\operatorname{Con}\sf(ZF)$ holds, then I don't see how your natural numbers could ever satisfy $\operatorname{Con}\sf(ZF)$. – Asaf Karagila Dec 13 '17 at 15:41
• @user21820 How do you know that Con(ZFC) is true? That's what Asaf means by metatheory. – Noah Schweber Dec 13 '17 at 15:41
• @user21820 If you prefer, when we say "metasystem" just think "reality." – Noah Schweber Dec 13 '17 at 15:55