# Isn't it problematic to cite the Gödel sentence as a proposition asserting 'This sentence is unprovable' since it isn't really on point?

In the proof of Gödel's incompleteness theorem the Diagonalization Lemma is applied to the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that

$F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)$,

where F is the formal system and $⌈G_F⌉$ the Gödel number of $G_F$. To rest of the proof is a fairly straightforward task.

What I'm concerned about is the interpretation of $G_F$: Many sources interpret the assertion of it to be 'This sentence is unprovable'. I know, $¬Prov_F(⌈G_F⌉)$ seems to suggest this but strictly speaking the Diagonalization lemma purports $¬Prov_F(⌈G_F⌉)$ follows from $G_F$ and vice versa, nothing more.

So what does it mean for a sentence to assert its own unprovability? A proposition saying 'This sentence is unprovable' seems to have no content since 'This sentence' is not specified. What sentence is unprovable?

Just to stress, I've no problem with the proof of Gödel's incompleteness theorem. I just don't understand the expression in the metalanguage.

For example, "$P$" and "$P$ is true" mean the same thing (this is called "the deflationary theory of truth" in the philosophy-of-language literature).
In that case, of course, $G_F$ really is the same as the sentence "$G_F$ is not provable in $F$", and so does assert its own $F$-unprovability. Of course, the claim I've highlighted isn't actually universally accepted (which is why I highlighted it), but I think it is a very reasonable thing, especially for first-read intuitions.
The sentence is a specific one, and it is in fact specified. Let's say it happens to have Gödel number $12345$ (the actual number depends on the specific encoding used, and is likely to be huge). Its interpretation is that the sentence constructed in a certain way (which happens to be the one with Gödel number $12345$) is unprovable in the system.