5
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ I now had I look at Enderton’s book, and I am quite puzzled: as far as I can tell, the contents of the book gets nowhere near the tools needed to (affirmatively) solve the exercise. $\endgroup$ Commented Jun 22, 2020 at 13:55
  • $\begingroup$ Was this question also in the 1972 version of the book, before the paper by Pudlak cited below? $\endgroup$
    – user44143
    Commented Jun 22, 2020 at 16:57
  • $\begingroup$ @Matt F: I checked the 1972 version of the book and, no, it wasn't. you made a good point. But still i don't know why Enderton has put this problem in the exercises. As Emil said, the book only covers 3 lob conditions which doesn't help. $\endgroup$
    – Ali
    Commented Jun 23, 2020 at 6:46

1 Answer 1

7
$\begingroup$

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.

[2] Petr Hájek, Pavel Pudlák: Metamathematics of first-order arithmetic, Springer, 1994, 2nd ed. 1998, 3rd ed. Cambridge Univ. Press 2017.

$\endgroup$

You must log in to answer this question.

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