This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure:
So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at this point one is done.
Then, as that unproven sentence contains the claim that this (the unprovable-ness) would happen, one is in some sense justified to say "So the statement really is true, but still, it's unprovable within the theory". Now here is my problem: I'm very unsure in which sense this notion of truth which somewhat comes from outside the theory is sensible. There is a note on that point on the wikipedia page but I don't really comprehend it.
The word "true" is used disquotationally here: the Gödel sentence is true in this sense because it "asserts its own unprovability and it is indeed unprovable" (Smoryński 1977 p. 825; also see Franzén 2005 pp. 28–33). It is also possible to read "GT is true" in the formal sense that primitive recursive arithmetic proves the implication Con(T)→GT, where Con(T) is a canonical sentence asserting the consistency of T (Smoryński 1977 p. 840, Kikuchi and Tanaka 1994 p. 403)
So I can see that if one is technically aware that one is now talking in a meta language, that one has introduced a new "true". But then again (a) if one reflects on the fact that one draws such technicals conclusions outside of the initial freamework, then it seems to me one should really introduce another meta-meta-language. And (b) isn't it really just a little ambiguous to say "Gödels incompleteness theorems says that there are true statements, which can't be proven within a certain strong theory"?
I'd be thankful if someone could elaborate on that.