I am confused about one of the standard proofs of this theorem that I've seen. I believe it's a small thing that I missing as authors seem to skip straight through it. The proof I am referring to is the one that:
(1) encodes formulas of a logical system (such as RA) using Gödel numbering, having agreed on numerical labels for the symbols of the language. Then encodes sequences using the encoding for formulas.
(2) is able to encode '$p$ is a proof of $q$'
(3) is able to encode 'there exists a proof of $p$'
(4) creates an 'I am not provable' sentence
It's the nature of (2) and (3) that I am iffy about:
- are we talking about merely encoding those statements, or is it about whether the system able to 'check' whether $p$ is a proof of $q$, in some sort of computable way? I can see how it would do so, it decodes the list of formulas presented by $p$ using arithmetic, and checks whether they follow the rules of logic established in advance by our system, also using arithmetic.
- if the latter on my previous question, how does one get (3) from (2)? It seems authors go from checking $p$ proves $q$ to 'given $q$, we can establish whether it has a proof or not in the system' (or the system can, viewing all of this has code/arithmetic), but it's not clear to me how exactly?
I would appreciate any help!
For simplicity, throughout I'll conflate a natural number $k$ with the corresponding numeral $\underline{k}$. Also I'll talk about $\mathsf{PA}$ instead of $\mathsf{RA}$, since I don't know what the latter is and the argument is the same for all appropriate theories.
I'm not sure I quite understand your first question, but I believe the following will clear things up - the key point being the difference between definability and provability, and the subsequent notion of representability which connects the two. We have two different objects at play here: the structure $\mathfrak{N}=(\mathbb{N};+,\times)$, that is the standard model of arithmetic, and the theory $\mathsf{PA}$. "Talking about provability in $\mathsf{PA}$" amounts to two observations, which I've separated below:
First, we have the purely model-theoretic fact.
Fixing an appropriate Godel numbering system $\ulcorner\cdot\urcorner$, we whip up a formula $\varphi(x,y)$ in the language of arithmetic such that for each finite string of symbols $\alpha$ and each finite string of finite strings of symbols $\pi$ we have $$\mathfrak{N}\models\varphi(\ulcorner \pi\urcorner, \ulcorner\alpha\urcorner)\quad\iff\quad\mbox{$\alpha$ is a sentence and $\pi$ is a $\mathsf{PA}$-proof of $\alpha$}.$$ Note that the theory is not involved yet. $\mathsf{PA}$-provability then corresponds to the formula $$\psi(y)\equiv \exists x\varphi(x,y).$$ What this all says is that the "is-a-$\mathsf{PA}$-proof-of" relation and the "is-$\mathsf{PA}$-provable" predicate are each definable in the structure $\mathfrak{N}$ - after "pushing through" the Godel numbering system, that is.
Now we show that $\mathsf{PA}$ "understands" the formula $\varphi$ we've produced above - or at least, understands "basic facts" about $\mathsf{PA}$. Specifically, we claim that for every $m,n\in\mathbb{N}$ we have $$\mathfrak{N}\models\varphi(m,n)\quad\iff\quad \mathsf{PA}\vdash\varphi(m,n)$$ and $$\mathfrak{N}\models\neg\varphi(m,n)\quad\iff\quad\mathsf{PA}\vdash\neg\varphi(m,n).$$ In jargon, the relation $\varphi$ is representable in $\mathsf{PA}$.
With this in hand, we'll be able to prove the first incompleteness theorem: we prove the diagonal lemma and apply it to the formula $\neg\psi$, and then a quick analysis gives $\mathsf{PA}\not\vdash\theta$ and $\mathsf{PA}\not\vdash\neg\theta$. These last two steps are quite short. By far the longest part of the proof is constructing the desired $\varphi$.
A couple final comments:
First, Rosser's improvement uses the same idea, except it looks at something more compicated than $\psi$. First we whip up a formula $\upsilon(x,y)$ which defines in $\mathfrak{N}$ the relation "$y$ is the Godel number of the sentence with Godel number $x$" and which is $\mathsf{PA}$-representable. This takes some work, but not nearly as much as whipping up $\varphi$. Then we apply the diagonal lemma, not to $\neg\psi(y)$, but to the more complicated formula $$\chi(y)\equiv\forall x(\varphi(x,y)\rightarrow\exists z,w(z<x\wedge\upsilon(y,w)\wedge \varphi(z, w))$$ ("for every proof of me there is a shorter disproof of me"). A minor modification of Godel's original "quick analysis" mentioned above then shows that the resulting fixed point is $\mathsf{PA}$-undecidable using only the hypothesis that $\mathsf{PA}$ is consistent (as opposed to $\omega$-consistent).
Second, it's worth noting that when a formula $\gamma(x,y)$ is representable in $\mathsf{PA}$, the formula $\exists x\gamma(x,y)$ will not in general be representable - but it will be "half-representable." Specifically, we'll have for each $m\in\mathbb{N}$ that $$\mathfrak{N}\models\exists x\gamma(x,m)\quad\implies\quad\mathsf{PA}\vdash\exists x\gamma(x,m).$$ In particular, each $\mathsf{PA}$-provable sentence is $\mathsf{PA}$-provably $\mathsf{PA}$-provable; in the modal logic of provability this is expressed by the axiom $\Box p\rightarrow \Box\Box p.$