first-order-logiclogicprovability
My question is: within a system $S$ where $S$ is any extension of $Q$ (Robinson's Arithmetic), and when $P(y)$ is a provability predicate for $S$, when is $(X \rightarrow P(X))$ provable?
By definition of a provability predicate, it is always the case that if $X$ is provable in $S$ then $P(X)$ is provable in $S$. But this, as I understand it, is not the same as $(X \rightarrow P(X))$ being provable in $S$. So when is this the case?
See Löb's Theorem, for example in :
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 :
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
- $\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); 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 :
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.
The usual way to define truth is due to Tarski. Given a structure $M$ (i.e. a set with operations and relations), we recursively define $M \models \phi$, meaning $\phi$ is true in $M$. For concreteness, let's consider the natural numbers $N = (\mathbb N, +, \times, 0, 1, <)$:
$N \models a + b = c$ if it the output of the binary function $+$ on input $(a,b)$ is $c$. Similarly for $N \models a \times b = c$.
$N \models a < b$ if $(a,b)$ is in the set $\mathord< \mathbin{\subseteq} \mathbb N^2$.
$N \models \phi \land \psi$ if $N \models \phi$ and $N \models \psi$ and $N \models \phi \lor \psi$ if $N \models \phi$ or $N \models \psi$.
$N \models \neg \phi$ if it is not the case that $N \models \phi$.
$N \models \exists x \phi(x)$ if there is some $a \in \mathbb N$ so that $N \models \phi(a)$ and $N \models \forall x \phi(x)$ if for all $a \in \mathbb N$ we have $N \models \phi(a)$.
In other words, truth is defined exactly how you would expect; symbols in the language correspond to certain constants, functions, and relations in the structure and truth is based upon that connection.
Provability, on the other hand, isn't a property of structures. Instead, it's a property of theories. If $T$ is a theory, meaning a set of sentences in some fixed language, then we can define a provability relation $T \vdash \phi$. There are many ways to do the details here to match with our intuitive notion of provability. But the important things are that the provability relation should be closed under valid inference rules (e.g. if $T \vdash \phi$ and $T \vdash \phi \rightarrow \psi$, then $T \vdash \psi$), that the axioms of $T$ are provable (if $\phi \in T$ then $T \vdash \phi$), and that logical validities (statements true in any structure) are provable.
We can now ask about how provability and truth relate. Any definition of provability worth a damn will be sound. This means that if $M$ is a model of $T$ (i.e. every axiom of $T$ is true in $M$, when interpreted appropriately), then $T \vdash \phi$ implies $M \models \phi$. In other other words, if we have proved something, then we know it is true. Moreover, as Gödel showed, first-order logic is complete. This means that if every model $M$ of $T$ has $M \models \phi$, then $T \vdash \phi$.
On a final note, it's very common to see people refer to truth without indicating a structure they are working in or refer to provability without indicating a theory they are working from. In the former situation, it's usually clear what structure is implicitly being used. For instance, the statement "17 is prime" is referring to the natural numbers, and can be translated to a formal statement something like $N \models \forall x < 17\, \exists y \le 17 \ (x \times y = 17 \rightarrow x = 1)$.
In the latter situation, when referring to provability, some implicit background of commonly accepted mathematics is assumed. When we say that the intermediate value theorem is provable, we mean that there is a proof of the IVT from some commonly accepted basic principles.
Best Answer
One instance where this holds is when $P$ is $\Sigma_1$ and $S$ is a bit stronger than $Q$: a sufficiently strong (consistent, recursively axiomatizable) theory of arithmetic (PA is massive overkill) proves that it proves every true $\Sigma_1$ sentence. I don't recall if $Q$ has this property.
We can get a partial reversal under a correctness assumption on $S$. Suppose $T$ is an appropriately-strong theory which proves "$S$ is sound" *(this is really a scheme: $T$ proves $P(X)\rightarrow X$ for each $X$, where again $P$ is the provability predicate for $S$)*. Then for each $X$, $T$ proves "If $S$ proves $X\rightarrow P(X)$, then $X\iff P(X)$," and $P(X)$ is a $\Sigma_1$ sentence regardless of the complexity of $X$.
Another example occurs whenever $S$ proves its own inconsistency, which can happen even if $S$ is consistent (consider PA + $\neg$Con(PA)). In this case $S$ trivially proves $X\rightarrow P(X)$ for each $X$, since $S$ proves $P(X)$ for each $X$.
Meanwhile, when you write
you're absolutely right. Let's assume PA is sound. We know that the $\Sigma_2$-theory of arithmetic is not recursively enumerable, but the set of PA-provable $\Sigma_2$-sentences is; thus, since by soundness there is no false $\Sigma_2$-sentence which is PA-provable, there must be a true $\Sigma_2$-sentence which is not PA-provable. Letting $X$ be such a sentence, we have (again, by soundness of PA) that PA can't prove $X\rightarrow P(X)$.