Decidability of Gödel sentences.

Question

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?

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.