5
$\begingroup$

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?

Improve this question
$\endgroup$
8
  • $\begingroup$ Is it true that for every sentence $\phi$, $Q\vdash Pr_Q(\ulcorner \bot\urcorner)\to Pr_Q(\ulcorner \phi\urcorner)$ ? If that's the case then Lob's theorem is provable in $Q$. $\endgroup$
    – Erfan Khaniki
    Commented May 1, 2017 at 9:04
  • 1
    $\begingroup$ What is a "recursive sentence"? $\endgroup$
    – Noah Schweber
    Commented May 1, 2017 at 14:00
  • $\begingroup$ @NoahSchweber Here I take a recursive sentence to be a $\Delta_1$-sentence. Is that not common? $\endgroup$
    – Frode Alfson Bjørdal
    Commented May 1, 2017 at 14:56
  • $\begingroup$ I haven't personally seen it used that way, but that doesn't mean it's not common; I just didn't know what you meant. $\endgroup$
    – Noah Schweber
    Commented May 1, 2017 at 16:17
  • $\begingroup$ I see now that there is different usage. Here is one article which talks about $\Delta_1$ formulas: en.wikipedia.org/wiki/Reverse_mathematics#The_base_system_RCA0. But now that you bring it up I see that it is probably best to use $\Delta_{n}$ only for sets defined both by $\Sigma{n}$ and $\Pi_{n}$ formulas, as the criteria for identifying formulas are purely syntactical. $\endgroup$
    – Frode Alfson Bjørdal
    Commented May 1, 2017 at 16:31

1 Answer 1

Reset to default
6
$\begingroup$

No consistent recursively axiomatized extension $T$ of $Q$ can prove $\mathrm{Pr}_T\ulcorner\bot\urcorner\to\bot$, that is, $\mathrm{Con}_T$.

In fact, no consistent r.e. theory $T$ can interpret $Q+\mathrm{Con}_T$.

In fact, no consistent r.e. theory $T$ can interpret $Q+\{\mathrm{RCon}_T(\overline n):n\in\mathbb N\}$, where $\mathrm{RCon}_T(x)$ denotes the consistency of $T$ with respect to proofs using only formulas of “complexity” $x$. See Pudlák’s Cuts, Consistency Statements and Interpretations. (He proves it for interpretations on a cut, but this does not really make a difference.)

Improve this answer
$\endgroup$

You must log in to answer this question.

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