1
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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

$\endgroup$
11
  • $\begingroup$ 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. :-) $\endgroup$ – Asaf Karagila♦ Jul 17 '15 at 20:41
  • $\begingroup$ @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. =) $\endgroup$ – user21820 Dec 13 '17 at 15:39
  • $\begingroup$ @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)$. $\endgroup$ – Asaf Karagila♦ Dec 13 '17 at 15:41
  • $\begingroup$ @user21820 How do you know that Con(ZFC) is true? That's what Asaf means by metatheory. $\endgroup$ – Noah Schweber Dec 13 '17 at 15:41
  • 1
    $\begingroup$ @user21820 If you prefer, when we say "metasystem" just think "reality." $\endgroup$ – Noah Schweber Dec 13 '17 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.