1
$\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
$\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 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
$\endgroup$
  • $\begingroup$ Thank you, and great example. $\endgroup$ – Eoin Feb 13 at 19:55

This site is temporarily in read only mode and not accepting new answers.

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