It is an odd and arguably unacceptable situation that $PA$ does not have $\vdash_{PA}(Pr_{PA}\ulcorner A\urcorner\to A)$ for false recursive sentences $A$.

However, it is not clear to me that Löb's theorem is already derivable in Robinson arithmetic $Q$, for one cannot assume that the provability predicate of $Q$ obeys all the Löb derivability conditions. (Compare to these matter question A question on the provability predicate of Q).

Are there natural omega consistent extensions $Q*$ of $Q$ such $\vdash_{Q*}(Pr_{Q*}\ulcorner A\urcorner\to A)$ for all $\Delta_1$ sentences?

3more comments