I'm working through Peter Smith's book, 'An Introduction to Godel's Theorems'.
One small issue I've encountered is how the notion of expressibility is used to prove the incompleteness of Peano Arithmetic. In particular, the relation $Gdl(m,n)$, which holds iff $m$ is the super g.n. of a proof of the formula with g.n. $n$, is primitive recursive and thereby expressible by a $L_A$. Say Gdl(x,y) expresses $Gdl$. Let G be the diagonalization of the formula
That is to say, G is U($\ulcorner$U$\urcorner$) which may be written as $\forall$x$\neg$Gdl(x,$\ulcorner$U$\urcorner$).
Now we wish to show that G is true iff G is unprovable.
Here's the issue that concerns me. Smith says G is true iff there is no number $m$ such that $Gdl(m,\ulcorner U \urcorner)$. This doesn't quite seem true. In particular, Gdl(x,$\ulcorner$U$\urcorner$) might be satisfied by some element of the universe which is not actually a natural number. In this case, expressibility doesn't seem to play a role.
Any help is appreciated. I also have some broader questions on first-order logic which I've posted here.