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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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$.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Dear Dr. Hamkins, Thanks a lot for this nice proof $\endgroup$
    – Payam Seraji
    Commented 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.
    Commented Jan 15, 2020 at 5:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .