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
U(y)$=_{def} \forall$x$\neg$Gdl(x,y)
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.
$\mathsf{Gdl}$, the formal wff which expresses the numerical relation $Gdl$ is a wff of the INTERPRETED language $L_A$ where the domain over which the variables run is specified to be the standard natural numbers.
So $\mathsf{G}$, which is equivalent to $\mathsf{\forall x\neg Gld(x,\ulcorner\mathsf{U}\urcorner)}$, is true (true-in-$L_A$, if you prefer) if everything in the domain of the quantifier, which is already specified to be the natural numbers, satisfies $\mathsf{\neg Gld(x,\ulcorner\mathsf{U}\urcorner)}$, i.e. if no number $m$ satisfies $\mathsf{Gld(x,\ulcorner\mathsf{U}\urcorner)}$. Since $\mathsf{Gdl}$ expresses $Gdl$, that means if no number $m$ is such that ${Gld(m,\ulcorner\mathsf{U}\urcorner)}$. As I said.