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?

$\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$ May 1 '17 at 9:04
  • 1
    $\begingroup$ What is a "recursive sentence"? $\endgroup$ May 1 '17 at 14:00
  • $\begingroup$ @NoahSchweber Here I take a recursive sentence to be a $\Delta_1$-sentence. Is that not common? $\endgroup$
    – FAB
    May 1 '17 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$ May 1 '17 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$
    – FAB
    May 1 '17 at 16:31
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.)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.