# Unprovable sentence, but provably it is provable.

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

• 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. – Noah Schweber Feb 13 '19 at 19:47

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.