I am aware of the fact, that the following considerations can be done for various strong enough theories in various first-order languages. I am, however, only interested (for simplicity) in the case for first-order Peano arithmetic.
In the development done before proving Gödel's second incompleteness theorem in most textbooks, one constructs the proof predicate $\mathrm{Proof}(x,y)$ such that
$$\mathsf{PA}\vdash\phi\text{ iff there is an $m\in\mathbb N$ such that }\mathsf{PA}\vdash\mathrm{Proof}(n,m)\text{ where $n$ is the Gödel number of $\phi$}$$
where, with $\mathrm{Proof}(n,m)$, I mean to substitute the terms representing $n,m$ for $x,y$ in $\mathrm{Proof}$.
One may proceed to derive the provability predicate $\mathrm{Prf}$ from this by existentially quantifying the variable $y$ in $\mathrm{Proof}$ and to prove the Löb derivability conditions for this predicate, which then leads to the second incompleteness theorem.
What I am wondering about is the following: The approach to the first incompleteness theorem that I am most used to is to show that
$$\{n\in\mathbb N\mid n\text{ is the Gödel number of some $\phi$ such that }\mathsf{PA}\vdash\phi\}=T$$
is not representable in $\mathsf{PA}$, i.e. that there is no formula $\mathrm{R}(x)$ with one free variable $x$ in the language of arithmetic such that
- If $n\in T$, then $\mathsf{PA}\vdash R(n)$.
- If $n\not\in T$, then $\mathsf{PA}\vdash\neg R(n)$.
That means that the proof predicate $\mathrm{Prf}$ can not be a representation of the set $T$. Does this make the provability predicate less of a proper provability predicate? I would just like to put these things in order in my head.
Best Answer
What the facts you’ve laid out show is that PA cannot prove/refute every instance of the provability predicate. This should come as no surprise since the second incompleteness theorem says that it cannot refute any negative instance, much less every. So it is really PA that is failing here, not the predicate.
I think your error is going from “does not represent in PA” to “cannot be a representation of”. The former is a technical concept, whereas the latter, stripped of the crucial qualifier “in PA”, sounds a lot stronger than what the former actually means. For instance, the provablility predicate definitely defines $T$ in $\mathbb N,$ in the usual sense that it is true of $n$ if and only if $n\in T.$