This question is about the number system Godel used in his Incompleteness Theorem. It seems that the result of his theorem is that somethings (in mathematics) may never be provable, although they will still be true. I was listening to a lecture regarding the theorem and the presenter made the comment that during the number-encoding step the theorem was essentially transforming into a meta-language, which was outside the original symbol based language that the theorem is constructed in.
My understanding is that somethings may be proved when in a different meta-language if they are not provable in the language in which they are first modeled.
My question is this; if the G statement cannot be proved in the original language and axioms from where it is constructed, is the act of transforming the statement into Godel numbering what allows it to become provable? Is the proof happening in the arithmetic phase of the proof because that is a meta-language somehow where the proof can take place? Then do the results decode back into symbols to show that the statement is in fact true? I hope my question is clear.
"It seems that the result of [Gödel's] theorem is that some things (in mathematics) may never be provable". Not so. It is the result of Gödel's theorem that for any suitable theory $T$, there will be a sentence $G_T$ that $T$ itself can't decide -- i.e. $T$ itself can't prove $G_T$ and $T$ can't prove $\neg G_T$. But that leaves it wide open that $G_T$ can be proved in some other way, perhaps in some natural expansion of $T$ or in some other theory.
It can help to shift focus for a moment from the standardly constructed Gödel sentence $G_T$ for a suitable given theory $T$ to the consistency sentence $Con(T)$ (which roughly says that no number codes for a $T$-proof of absurdity). It will be fairly elementarily provable inside $T$ that $G_T \equiv Con(T)$. So we have the second incompleteness result: assuming it is consistent, $T$ can't prove $Con(T)$ or $\neg Con(T)$. But that leaves it wide open that $Con(T)$ can be proved in some other way. For a simple example, standard first-order arithmetic $PA$ is incomplete -- it can't prove $Con(PA)$. But we believe that $PA$ is consistent. And, if we like, we can prove $PA$ is consistent in some richer theory like a weak set theory. So we think $Con(PA)$ is true. And, a further step, our reasons for thinking it true can be formalised in our richer set theory which can then prove the arithmetical coding of the claim in the form $Con(PA)$.
Now, varying your question just a bit: "if the $Con(PA)$ statement cannot be proved in the original language and axioms from where it is constructed, is the act of transforming the statement into Godel numbering what allows it to become provable"? No. That rather gets things upside down. It is trick of "transforming" the claim PA-is-consistent into a formal arithmetical statement via Gödel numbering which enables us to construct the formal statement $Con(PA)$ and which is used in showing that it can't be proved in the relevant theory $T$. On the other hand, what makes PA-is-consistent true, and provably true in a richer context, need not involve any Gödel numbering (that will only come back into the picture if we also want to show that one particular way of expressing that, namely $Con(PA)$, is also provable in the richer context).
For more see e.g. my Gödel Without (Too Many) Tears, downloadable from https://logicmatters.net/igt