A sentence asserting about itself that if it is provable, then it is true

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}$.

1. Let $\vdash A \leftrightarrow ({\rm Pr}(n)\rightarrow A)$. [This is the assumption we start with]
2. 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$".]
3. 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.]
4. From 1 and 2, $\vdash {\rm Pr}(n)\rightarrow A$.
5. 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:

1. 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?
2. Or, if my interpretation of the argument is incorrect and the argument works, how should the argument be expressed clearly and formally?

Solution 1:

See Löb's Theorem, for example in :

• Torkel Franzén, Godel's theorem : An incomplete guide to its use and abuse (2005), page 101-102, that seems to me well explained and detailed :

Suppose we produce a provable fixpoint for the property of being a theorem of $\mathsf {PA}$, instead of (as in Gödel's proof) the property of not being theorem of $\mathsf {PA}$. In other words, let $H$ (for Leon Henkin, who first raised this question) be an arithmetical statement formalizing "this statement is provable in $\mathsf {PA}$." Is $H$ provable in $\mathsf {PA}$ or not ? Reflecting on the meaning of $H$ only yields that $H$ is true if and only if it is provable in $\mathsf {PA}$, which doesn't get us anywhere, and it may at first seem hopeless to decide whether this strange self-referential sentence is provable in $\mathsf {PA}$ or not.

Löb solved the question of the provability of $H$ by showing that it holds more generally that if $\mathsf {PA}$ proves "if $\mathsf {PA}$ proves $A$ then $A$", then $\mathsf {PA}$ proves $A$ [my addition : if $\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$, then $\mathsf {PA} \vdash A$] (so that in particular the Henkin sentence is indeed provable in $\mathsf {PA}$).

To see this, consider the theory $\mathsf {PA} + \lnot A$. We are assuming that $\mathsf {PA}$ proves "if $\mathsf {PA}$ proves $A$ then $A$," which implies "if $\lnot A$ then $\mathsf {PA}$ does not prove $A$." But this in turn implies "if $\lnot A$ then $\mathsf {PA} + \lnot A$ is consistent," so $\mathsf {PA} + \lnot A$ proves the consistency of $\mathsf {PA} + \lnot A$, and thus is in fact inconsistent, implying that $\mathsf {PA}$ proves $A$. The same argument applies to any theory $T$ for which the second incompleteness theorem holds.

The second incompleteness theorem is a special case of Löb's theorem, as we see by choosing $A$ in the formulation of the theorem as a logical contradiction "$B$ and $\lnot B$." For such an $A$, "$\mathsf {PA}$ proves $A$" is the same as saying "$\mathsf {PA}$ is inconsistent," and any hypothetical statement "if $C$ then $A$" is logically equivalent to $\lnot C$. Thus, Löb's theorem tells us that if $\mathsf {PA}$ proves "$\mathsf {PA}$ is not inconsistent" then $\mathsf {PA}$ is inconsistent, or in other words, if $\mathsf {PA}$ is consistent then $\mathsf {PA}$ does not prove "$\mathsf {PA}$ is consistent."

Löb's theorem gives us a rather odd principle for proving theorems about the natural numbers. In order to prove $A$, it is admissible to assume as a premise that $A$ is provable in $\mathsf {PA}$, as long as the argument is one that can be formalized in $\mathsf {PA}$. For if there is a proof in $\mathsf {PA}$ of "if there is a proof in $\mathsf {PA}$ of $A$ then $A$" then there is a proof in $\mathsf {PA}$ of $A$. A similar principle holds, for example, for $\mathsf {ZFC}$. This principle doesn't have any known application in proving any ordinary mathematical theorems about primes or other matters of traditional mathematical interest, but it does have uses in logic.

Löb's principle may seem baffling rather than just odd. How can it be admissible, in proving $A$, to assume that $A$ is provable in $\mathsf {PA}$? After all, whatever is provable in $\mathsf {PA}$ is true, so can't we then conclude without further ado that $A$ is true, and so prove $A$ without doing any reasoning at all? The essential point here is that it is admissible to assume that $A$ is provable in $\mathsf {PA}$ when proving $A$ only if the reasoning leading from the assumption that $A$ is provable in $\mathsf {PA}$ to the conclusion $A$ can in fact be carried out within $\mathsf {PA}$. That everything provable in $\mathsf {PA}$ is true is not something that can be established within $\mathsf {PA}$ itself, as is shown by the second incompleteness theorem. To say that, for example, $0 = 1$ is true if provable in $\mathsf {PA}$ is (given that $0$ is not equal to $1$) the same as saying that $0 = 1$ is not provable in $\mathsf {PA}$, or in other words that $\mathsf {PA}$ is consistent.

We can "formalize" Franzén argument :

1) assume : $\mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$

2) $\mathsf {PA} \vdash \lnot A \to \lnot \rm Pr_\mathsf{PA}(\ulcorner A \urcorner)$ --- from 1) by tautological implication

3) $\mathsf {PA} \vdash \lnot A \to \rm Cons (\mathsf{PA} + \lnot A)$

4) $\mathsf {PA} + \lnot A \vdash \rm Cons (\mathsf{PA} + \lnot A)$ --- contradiction

5) $\mathsf {PA} \vdash A$ --- from 4) by Reductio Ad Absurdum.

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 :

$\mathsf {PA} \vdash A \ \ $ iff $ \ \ \mathsf {PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner A \urcorner) \to A$.

See : George Boolos & John Burgess & Richard Jeffrey, Computability and Logic (5th ed - 2007), corollary to Löb’s theorem, page 237 :

Corollary 18.5 : Suppose that $\rm Pr_T(x)$ is a provability predicate for $T$. Then if $T \vdash H ↔ \rm Pr_T(\ulcorner H \urcorner)$, then $T \vdash H$.

Proof: Immediate from Löb’s theorem.

The conclusion following from BBJ's Corollary is :

the sentence $H$ asserting of itself that "it is provable" ($H ↔ \rm Pr_\mathsf{PA}(\ulcorner H \urcorner)$) is provable, and thus it is true and provable.

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 :

Going back to self-reference, we have seen that the sentence asserting its own unprovability is true and not provable. We now want to show that, under the conditions stated above [the three Löb’s properties of $\rm Pr_T$], the sentence asserting its own provability is true and provable. This provides an example of true self-referential statement which makes no use of negation. The general result is that, under the conditions stated above, a sentence $\psi(\overline x) \to \psi_x$ (asserting that if $\psi_x$ is provable then it is true, and thus expressing a form of soundness) is provable if and only if $\psi_x$ is (Löb's Theorem). [...]

Since the formula that asserts its own provability has the property that $\vdash_\mathcal F \psi(\overline x) \leftrightarrow \psi_x$, we have in particular that $\psi(\overline x) \to \psi_x$ is provable, and then so is $\psi_x$ itself, by Löb's Theorem.

Up to now, "all works" ...

A similar example, relying on the same conditions on the provability predicate but not using Gödel's Second Theorem, is the sentence asserting of itself that if it is provable then it is true, i.e. $\vdash_\mathcal F \psi(\overline x) \leftrightarrow (\psi(\overline x) \to \psi_x)$.

Suppose $\psi_x$ is provable. Then $\vdash_\mathcal F \psi(\overline x)$ by representability of provability, and $\vdash_\mathcal F (\psi(\overline x) \to \psi_x)$ by definition of $\psi_x$. By modus ponens, $\vdash_\mathcal F \psi_x$. Thus we have proved that if $\psi_x$ is provable, i.e. if $\psi(\overline x)$ holds, then so does $\psi_x$. This establishes that if $\psi_x$ is provable then it is true. By $\psi_x$ asserts exactly this, and thus it is true and provable.

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).

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 :

the sentence $O$ asserting of itself that "if it is provable then it is true" is provable, and thus it is true and provable.

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 :

This establishes that if $O$ is provable then it is true.

We can "formalize" the proof in $\mathsf{PA}$, and thus :

$\mathsf{PA} \vdash \rm Pr_\mathsf{PA}(\ulcorner O \urcorner) \to O$.

Applying Löb's theorem, we conclude with :

$\mathsf{PA} \vdash O$.

Odifreddi again :

But $O$ asserts exactly this, and thus it is true and provable.

Solution 2:

This is perhaps similar in spirit to Andreas's answer. First of all, as observed by DanielV in a comment, $A\leftrightarrow (B\rightarrow A)$ is propositionally equivalent to $A\lor B$. (So we don't need to misapply the fixed point theorem to get such an $A$: we can take any formal theorem $A$ and will have that $\vdash A\leftrightarrow (P(A)\rightarrow A)$.)

Now our problem is that $\vdash A\lor P(A)$ does not imply that $\vdash A$ or $\vdash P(A)$. We can take the standard Gödel sentence $G$ as our $A$. Recall that this satisfies $\vdash G\leftrightarrow \lnot P(G)$. So $\vdash [G\lor P(G)]\leftrightarrow [\lnot P(G)\lor P(G)]$, and thus we do have that $$ \vdash G\lor P(G) , $$ even though $G$ is not a formal theorem.

So while every $A$ with $\vdash A$ will satisfy $\vdash A\leftrightarrow (P(A)\rightarrow A)$, there are also other such $A$'s that are not formal theorems. If our theory is arithmetically sound, then all $A$'s are of one of these two types:

If $\vdash A\leftrightarrow (P(A)\rightarrow A)$, then $\vdash A$ or $A$ is true and undecidable ($\not\vdash A, \not\vdash \lnot A$).

Update: I've now read the paragraph in Odifreddi you are referring to, and I can confirm that your summary is accurate. In particular, the passage "Suppose that $A$ is provable ... [then] $\vdash A$", which, as you rightly pointed out, isn't saying anything, gets summarized as "we have shown that if $A$ is provable, then ... $A$ holds [which I interpret as $\omega\models A$]," which of course is something else entirely.

This whole example is intended to be a variation on Löb's theorem, and I suspect Odifreddi simply didn't think very carefully about this paragraph and got misled by some formal analogy.

Solution 3:

Are there any background assumptions about the formal system, beyond mere consistency? For example, is it assumed that the system proves only truths? Without some such assumption, the result seems to fail. Here's an example.

Let $T$ be the theory obtained by adding to Peano Arithmetic (PA) the axiom that PA is inconsistent. This $T$ is consistent (by Gödel's second incompleteness theorem), but it easily proves its own inconsistency. Now let $A$ be some refutable (in PA) sentence, say $0=1$. Then $A$ is neither provable (in $T$) nor true. Nevertheless, it and its Gödel number $n$ satisfy $\vdash_T(A\leftrightarrow(\text{Pr}_T(n)\to A))$. The reason is that $T$ refutes $A$ but proves $\text{Pr}_T(n)$ because it proves its own inconsistency.