Unprovable sentence, but provably it is provable.

Question

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$?

Answer 1

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.