Letting $\text{Pr}(x)$ be a formula that weakly represents the set $\{x:x\text{ is a Gödel code of a provable sentence in PA}\}$, where PA means Peano Arithmetic.

Gödel's first incompleteness theorem shows that there is a sentence $\phi$ such that $$\text{PA}\vdash (\phi \leftrightarrow \neg \text{Pr}(\ulcorner \phi \urcorner)).$$ The theorem shows that $\phi$ is true but not provable in PA.

Now consider the following two sentences $\alpha$ and $\beta$ such that: $$ \text{PA}\vdash(\alpha \leftrightarrow \text{Pr}(\ulcorner \alpha\urcorner)\vee \text{Pr}(\ulcorner\text{Pr}(\ulcorner \alpha\urcorner) \urcorner)) \quad\text{and}\quad \text{PA}\vdash(\beta \leftrightarrow \text{Pr}(\ulcorner \beta\urcorner)\wedge \text{Pr}(\ulcorner\text{Pr}(\ulcorner \beta\urcorner) \urcorner)).$$ Is $\alpha$ (resp. $\beta$) decidable in PA? Is $\alpha$ (resp. $\beta$) true?


1 Answer 1


Generally, positive self-referentiality with the provability relation results in PA theorems (so there's a bit of asymmetry here). Specifically, Lob's theorem says that whenever PA proves $Pr(\ulcorner\varphi\urcorner)\rightarrow\varphi$ then PA already proves $\varphi$.

This immediately gives that PA proves $\alpha$. As for $\beta$, PA proves that PA is $\Sigma_1$-complete, so in particular PA proves $Pr(\ulcorner\varphi\urcorner)\rightarrow Pr(\ulcorner Pr(\ulcorner\varphi\urcorner)\urcorner)$ for each $\varphi$; so PA proves $Pr(\ulcorner\beta\urcorner)\rightarrow\beta$, and we may again use Lob's theorem to conclude that PA proves $\beta$.

Incidentally, Lob's theorem does use a mild assumption on the provability predicate; there are pathological things one might call "provability predicates" to which it doesn't apply. See the discussion at this earlier MSE question.


You must log in to answer this question.

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