In $\S$II.2 (vol. 1, p. 170) of his book on classical recursion theory, Odifreddi claims that the sentence asserting of itself that if it is provable then it is true "is true and provable." His argument (slightly rephrased) is as follows:
"Let
$\vdash A \leftrightarrow ({\rm Pr}(n)\rightarrow A),\ \ \ \ $
where $n$ is the Gödel number of $A$ and $\rm Pr$ is the provability predicate. Suppose $A$ is provable. Then $\vdash {\rm Pr}(n)$ by the representability of provability, and by the definition of $A$, $\vdash {\rm Pr}(n)\rightarrow A$. Therefore, $\vdash A$. Thus we have proved that if $A$ is provable, i.e., if ${\rm Pr}(n)$ holds, then so does $A$. So, if $A$ is provable then it is true. But this is what $A$ asserts, so it is true and provable."
To me, it seems that this argument makes no sense, as we start with $\vdash A$ and infer $\vdash A$, which implies nothing. Also, I don't see how such a sentence $A$ could be constructed. The usual diagonalization argument will construct a sentence $A$ such that $\vdash A \leftrightarrow Q(n)$ for any representable predicate $Q$, but truth is not representable. Can anyone clarify this statement and proof?
Addendum: To show the problem with the argument more clearly, I will rewrite it in a more formal way. Comments are in brackets. The turnstile, $\vdash$, represents provability in a given formal system $\cal F$; Odifreddi writes it as $\vdash_{\cal F}$.
- Let $\vdash A \leftrightarrow ({\rm Pr}(n)\rightarrow A)$. [This is the assumption we start with]
- Assume $\vdash A$. [This is the assumption that $A$ is provable, made as part of the argument. The words "A is provable" are synonymous with "$\vdash A$".]
- From 2, $\vdash {\rm Pr}(n)$. [This follows from 2 by a standard rule of inference of provability logic, as discussed on p. 169 of Odifreddi.]
- From 1 and 2, $\vdash {\rm Pr}(n)\rightarrow A$.
- From 3 and 4, $\vdash A$.
These steps are all correct, but the inference from 2 to 5 gets us nothing, as the conclusion is the same as the hypothesis. Now, Odifreddi says (rephrased) that "if $A$ is provable, i.e., if ${\rm Pr}(n)$ holds, then so does $A$." But we cannot conclude that $A$ holds in the sense of being true, because a priori, there is no truth within $\cal F$ (it's just a formal system.) Assuming that ${\rm Pr}(n)$ is expressed in the language of arithmetic, and that this language is contained in that of $\cal F$, we can talk about the truth of ${\rm Pr}(n)$, but only by re-expressing it as a statement about natural numbers. To formalize this, write the statement that ${\rm Pr}(n)$ is true as a statement about natural numbers as "$\omega \vDash {\rm Pr}(n)$." Then, we can conclude that
$\qquad\qquad\qquad\qquad\qquad\qquad$ If $\vdash A$, then $\vdash A$,
or
$\qquad\qquad\qquad\qquad\qquad\qquad$ If $\omega \vDash {\rm Pr}(n)$, then $\vdash A$,
since these are both different ways of expressing the tautology that, if $A$ is provable in $\cal F$, then it is provable in $\cal F$. But we cannot conclude that
$\qquad\qquad\qquad\qquad\qquad\qquad$ If $\vdash {\rm Pr}(n)$, then $\vdash A$,
since the argument does not start with the assumption $\vdash {\rm Pr}(n)$.
So, I would like to ask:
- Assuming that Odifreddi's argument is wrong, how can it be fixed; or is this impossible? Is Odifreddi's argument a garbled form of something recognizable?
- Or, if my interpretation of the argument is incorrect and the argument works, how should the argument be expressed clearly and formally?
Best Answer
See Löb's Theorem, for example in :
We can "formalize" Franzén argument :
assume : $\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$
$\mathsf {PA} \vdash \lnot A \to \lnot \rm Pr_\mathsf{PA}(\ulcorner A \urcorner)$ --- from 1) by tautological implication
$\mathsf {PA} \vdash \lnot A \to \rm Cons (\mathsf{PA} + \lnot A)$
$\mathsf {PA} + \lnot A \vdash \rm Cons (\mathsf{PA} + \lnot A)$ --- contradiction
Of course, from the tautology : $\varphi \to (\psi \to \varphi)$ we have : if $\mathsf {PA} \vdash A$, then $\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$; thus, we conclude with :
See : George Boolos & John Burgess & Richard Jeffrey, Computability and Logic (5th ed - 2007), corollary to Löb’s theorem, page 237 :
The conclusion following from BBJ's Corollary is :
By the Corollary above : if $T \vdash H ↔ \rm Pr_T(\ulcorner H \urcorner)$, then $T \vdash H$. But $H ↔ \rm Pr_T(\ulcorner H \urcorner)$ and thus, replacing $\rm Pr_T(\ulcorner H \urcorner)$ with $H$ in the premise, we have $T \vdash H ↔ H$, that is a tautology.
Thus, we conclude with $T \vdash H$ (under no assumptions) : $H$ is provable and thus, asserting its own provability, it is true. I.e. : it is true and provable.
According to the above discussion, we can go back to Odifreddi's claim.
The context [see page 169] is explicitly that of Löb’s theorem :
Up to now, "all works" ...
It is a version of "Henkin's paradox" with Provable in place of True ; see MH Lob, Solution of a Problem of Leon Henkin (1955); doi: 10.2307/2266895, jstor.
I'll try to "unwind" the argument above.
My first claim is that Odifreddi's "casual"reference to "an example [...] not using Gödel's Second Theorem" must be interpreted as pointing to a "semantical" argument.
I'll use $O$ for Odifreddi's sentence; thus, Odifreddi claims that :
Assume that $O$ is provable in $\mathsf{PA}$. Then, using the proof predicate to express this fact, we have that $\rm Pr_\mathsf{PA}(\ulcorner O \urcorner)$ is true.
If $\mathsf{PA}$ is sound, then $\rm Pr_\mathsf{PA}(\ulcorner O \urcorner) \to O$ must be true (this holds in general, for any sentence $S$ in place of $O$), and so, by modus ponens, we have that $O$ is true.
Thus, assuming the soundness of $\mathsf{PA}$, we have that $O$ is true.
Now, paraphrasing Odifreddi :
We can "formalize" the proof in $\mathsf{PA}$, and thus :
Applying Löb's theorem, we conclude with :
Odifreddi again :