2
$\begingroup$

Work in Peano Arithmetic, PA. Let Prov(n) be a standard proof predicate, so that $PA \vdash Prov(\ulcorner \phi \urcorner) \text{ iff } PA \vdash \phi$ .

By Löb's theorem, we know that if $PA \vdash Prov(\ulcorner \phi \urcorner) \rightarrow \phi$ then $PA \vdash \phi$. The fact that this is a theorem psychologically implies that we do not get the stronger result - if $PA \vdash Prov(\ulcorner \phi \urcorner)$ then $PA \vdash \phi$.

I am looking for counterexamples for the latter implication. Can anyone provide a sentence $\phi $ in PA such that $PA \vdash Prov(\ulcorner \phi \urcorner)$ and $PA \not\vdash \phi$?

| cite | improve this question | |
$\endgroup$
  • 1
    $\begingroup$ Your second sentence is making an assumption you're unwilling to make in the rest of the question. Namely, your second sentence claims "PA$\vdash Prov(\ulcorner\varphi\urcorner)$ iff PA$\vdash\varphi$," but then you ask whether we can have a $\varphi$ such that PA$\vdash Prov(\ulcorner\varphi\urcorner)$ but PA$\not\vdash\varphi$ - which would clearly contradict that initial claim! The issue is, per my answer below, your initial claim about how the provaibility predicate behaves assumes the $\Sigma_1$-soundness of PA, but your question itself doesn't. So there's a "metatheoretic mismatch" here. $\endgroup$ – Noah Schweber Feb 13 '19 at 19:47
4
$\begingroup$

No such $\varphi$ is known, nor is such (generally) believed to exist.

It is generally believed - similarly to how it is generally believed that PA is consistent - that no such $\varphi$ exists. Specifically, it is generally believed that PA is $\Sigma_1$-sound (= every $\Sigma_1$ sentence provable in PA is true), and indeed fully sound (= only proves true sentences). Of course, this tends to invoke at least a limited amount of Platonism; I'm not trying to argue the philosophical point, I just want to make it clear that the vast majority of mathematicians do not expect such a $\varphi$ to exist.

This is a nontrivial assumption, however: even PA+"PA is consistent" does not prove "PA is $\Sigma_1$-sound. So the phenomenon you're looking for, even though almost everybody thinks it won't happen, is still plausible at least in a very limited sense.

If we look beyond PA, however, we can easily find examples of this phenomenon. For instance, consider the theory $T=$ PA+"PA is inconsistent." By Godel's second incompleteness theorem, if PA is consistent then so is $T$, so $T\not\vdash 0=1$. However, we clearly have $T\vdash Prov_T(\ulcorner 0=1\urcorner)$.

That is, if PA is consistent, then PA has a consistent $\Sigma_1$-unsound extension.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thank you, and great example. $\endgroup$ – Eoin Feb 13 '19 at 19: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.