If i'm not wrong, the theory which Lob theorem applies to should be *sufficiently strong*, satisfying 3 "derivability" conditions, like PA.


$Q$ is the Robinson arithmetic.


I'm afraid $Q$, is not sufficiently strong, so the Lob theorem doesn't help for the following question :


If $ Q \vdash (\sigma \leftrightarrow Prb{Q}\sigma) $, does $Q \vdash \sigma$?


if the answer is no, the counterexample should be given, I assume.


Remark: my question is directly about excercise 3.7.1 of Enderton Introduction to logic.



Lob theorem for Robinson arithmetic
The answer is yes, and indeed, $Q$ is enough for Löb’s theorem:



> 
> **Theorem.** Let $T\supseteq Q$, and let $\tau\in\Sigma\_1$ define an axiom set for $T$ in $\mathbb N$. Then
> $$T\vdash(\Box\_\tau\phi\to\phi)\implies T\vdash\phi$$
> for all sentences $\phi$, where $\Box\_\tau$ denotes the formalized provability predicate for $\tau$.
> 
> 
> 


This was proved by Pudlák [1], even in a stronger form using restricted provability predicates (he states it for the second incompleteness theorem, but the argument for Löb’s theorem is essentially the same).


I will sketch the proof below. We rely on a few properties of Buss’s theory $S^1\_2$ (see e.g. Chapter V in Hájek and Pudlák [2]): $S^1\_2$ is a finitely axiomatizable fragment of arithmetic, it is interpretable in $Q$ on a definable cut, and it proves suitable versions of the usual Hilbert–Bernays–Löb derivability conditions.


Assume that $T\vdash\Box\_\tau\phi\to\phi$, and let $I$ be an interpretation of $S^1\_2$ in $Q$ on a definable cut. We have
$$T+\neg\phi\vdash\bigl(\neg\Box\_\tau\phi\bigr)^I$$
as $\Pi\_1$ statements are preserved downwards to cuts. Since $S^1\_2$ is finitely axiomatizable, there exists a finite theory
$$\tag{$\*$}U\subseteq T+\neg\phi$$
such that
$$\tag{$\*\*$}U\vdash(S^1\_2+\neg\Box\_\tau\phi)^I.$$
We have the following derivability conditions for all sentences $\psi$ and $\chi$:


$$\begin{gather}
\tag{1}U\vdash\psi\implies S^1\_2\vdash\Box\_U\psi,\\
\tag{2}S^1\_2\vdash\Box\_U(\psi\to\chi)\to(\Box\_U\psi\to\Box\_U\chi),\\
\tag{3}S^1\_2\vdash\Box\_U\psi\to\Box\_U(\Box\_U\psi)^I.
\end{gather}$$


Using Gödel’s diagonal lemma, let $\nu$ be a sentence such that


$$\tag{$\*{\*}\*$}S^1\_2\vdash\nu\leftrightarrow\neg\Box\_U\nu^I.$$


Then
$$\begin{align}
S^1\_2\vdash\neg\nu
&\to\Box\_U\nu^I&\text{by }&(\*{\*}\*)\\
&\to\Box\_U\bigl(\Box\_U\nu^I\bigr)^I&\text{by }&(3)\\
&\to\Box\_U\bigl(\Box\_U\nu^I\to\neg\nu\bigr)^I&\text{by }&(\*{\*}\*),(\*\*),(1)\\
&\to\Box\_U\neg\nu^I&\text{by }&(2)\\
&\to\Box\_U\bot&\text{by }&(2)\\
&\to\Box\_\tau\phi,
\end{align}$$
where the last step follows using the formalized deduction theorem from the fact that the axioms of $U$ consist of $\neg\phi$ and a finite list of axioms that satisfy $\tau$ (*provably* in $S^1\_2$ as $\tau$ is $\Sigma\_1$).


Thus,
$$\begin{align}
S^1\_2+\neg\Box\_\tau\phi&\vdash\nu,\\
U&\vdash\nu^I,&\text{by }&(\*\*)\\
S^1\_2&\vdash\Box\_U\nu^I,&\text{by }&(1)\\
S^1\_2&\vdash\neg\nu,&\text{by }&(\*{\*}\*)\\
U&\vdash\neg\nu^I,&\text{by }&(\*\*)\\
U&\vdash\bot,\\
T&\vdash\phi.
\end{align}$$


**References**


[1] Pavel Pudlák: *Cuts, consistency statements and interpretations*, Journal of Symbolic Logic 50 (1985), no. 2, pp. 423–441, DOI: [10.2307/2274231](https://doi.org/10.2307/2274231).


[2] Petr Hájek, Pavel Pudlák: *Metamathematics of first-order arithmetic*, Springer, 1994, 2nd ed. [1998](https://projecteuclid.org/euclid.pl/1235421926), 3rd ed. Cambridge Univ. Press [2017](https://doi.org/10.1017/9781316717271).


