3
$\begingroup$

I think it is well-known that $PA+\neg con(PA)$ is $\Pi_1$-conservative over $PA$ (for proof see Smorynski's article, 'the incompleteness theorems', in handbook of mathematical logic).

What can we say about $PA+\neg R_{PA}$ ? is it also $\Pi_1$-conservative over $PA$ ?($R_{PA}$ is the Rosser sentence for $PA$).

$\endgroup$

1 Answer 1

7
$\begingroup$

The Rosser sentence $R$ asserts, "for every proof of $R$ in PA, there is a smaller proof of $\neg R$." So $\neg R$ asserts, "there is a proof of $R$ in PA, with no smaller proof of $\neg R$."

In particular, we may deduce in $\text{PA}+\neg R$ that "for every proof of $\neg R$, there is a smaller proof of $R$". This is a $\Pi^0_1$ assertion.

But this implication is not provable in PA alone, since $R$ is known (under suitable consistency assumptions) to be strictly weaker than $\text{Con}(\text{PA})$, and in any model of $\text{PA}+R+\neg\text{Con}(\text{PA})$ there will be proofs of both $R$ and $\neg R$, but because $R$ is true, the smallest proof of $\neg R$ will be strictly smaller than the smallest proof of $R$.

$\endgroup$
2
  • $\begingroup$ Dear Dr. Hamkins, Thanks a lot for this nice proof $\endgroup$ Feb 10, 2015 at 18:27
  • $\begingroup$ @JoelDavidHamkins PA is conservative over HA (constructive Heyting Arithmetic) for $\Pi^0_2$ statements, that is PA proves the same $\Pi^0_2$ statements as HA. Is there something similar known for $\Sigma^0_2$ statements? $\endgroup$
    – VS.
    Jan 15, 2020 at 5:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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