>>4
That's bullshite. By metalanguage they usually mean just your initial language plus an additional axiom that says that your unprovable statement is, in fact, true. Or false, you will not have a contradiction either way. What's the point?
It's even more blatantly stupid when rephrased in the Halting Problem framework: so, you have found an undecidable program - i.e. one that can't be proven neither to halt nor not to halt. "Constructing a metalanguage" now means defining a new evaluator that is able to recognize this specific program and halt. Or go into the infinite loop, if you feel like it. And so you are magically able to solve a halting problem for this concrete program in your new shiny meta-evaluator - now you definetly know that it would halt (or not) and pre-analyze the program yourself and output just that if it was recognized. Wow, isn't that useful? A great success if you ask me!