How is a Godel sentence constructed?

I'm missing something in the argument for Godel's First Incompleteness Theorem, and I'm hoping that someone can clear up my muddle.

Godel constructs a sentence that is true iff it is unprovable. Here's my understanding of how he constructs it (taken from Peter Smith):

1. Consider U(y), with open variable y. U(y) is defined as "For all x, x does not code for a sequence of numbers that constitutes a proof of the diagonalization of the wff coded for by y."
2. The Godel sentence is the diagonalization of U(y). Meaning, the Godel sentence is "For all x, x does not code for a sequence of numbers that constitutes a proof of the diagonalization of U(y)."

The thing that I'm having trouble getting my head around is this: isn't U(y) an open sentence? Meaning, the variable 'y' is free in U(y). It was my understanding that open sentences aren't the sort of things that we could prove or not prove.

Now, I understand that the diagonalization of U(y) itself is not an open sentence, since it takes U(y) as its input. Still, I'm having trouble understanding what a proof of U(y) or its diagonalization would even look like. It seems trivial to me that the diagonalization of an open sentence wouldn't have a proof.

Can somebody check my understanding? What am I missing or misunderstanding? Thanks in advance.

-
Thinking about this some more, my inclination is that, no, it's not entirely shocking that a sentence constructed in this way (as the diagonalization of U(y) is) is unprovable. The real surprise is that the sentence is, as a consequence, true. Does that make sense? –  MBP Apr 24 '11 at 20:53
The best thing to do is forget about the "intuitive description" and look at the formal mathematics. –  quanta Apr 24 '11 at 21:33
U(y) is: If you consider y as an encoding of a statement Y(z) with one free variable, then there is no proof of Y(y). Then if u is an encoding of U(y), then U(u) essentially becomes: "There is no proof of U(u)." The statement U(y) is a general statement that might be true for some specific y, and not true for other specific y. But when the specific u is applied, we see Godel's result. –  Thomas Andrews Apr 24 '11 at 22:22
Nobody is stating anything about proving a statement with a free variable. Let's say $z$ encodes the statement Z(x)="x is a prime." Z(x) has a free variable, $x$, but the statement $U(z)$ states: "There does not exist a proof of Z(z)," which can be written as "There does not exist a proof that z is prime." –  Thomas Andrews Apr 24 '11 at 22:36

The actual Gödel sentence is obtained by taking the general formula $U_T(y)$, which has one free variable $y$, and substituting a particular closed term (that is, an expression of the form $1+1+\cdots+1$ with a certain number of 1s) into $y$. The term corresponding to a number $n$ might be denoted $\underline{n}$, $\dot{n}$, or $\ulcorner n \urcorner$ depending on the text you use. I will use $\ulcorner n \urcorner$, and I will use $\#(\phi)$ to refer to the Gödel number of a formula $\phi$.

In Gödel's original proof, the formula $U(y)$ is chosen so that, in the standard model, for any formula $\phi$, $U_T(\ulcorner \#(\phi) \urcorner)$ holds if and only if $\phi$ is not provable from the axioms of the theory $T$.

The number $n$ that is plugged in is chosen in such a way that that $U_T(\ulcorner n \urcorner)$ is equivalent, in $T$, to $U_T(\ulcorner \#(U_T(\ulcorner{}n\urcorner))\urcorner)$. The fact that such an $n$ exists is a consequence of the Diagonal Lemma.

The Gödel sentence is then defined to be the sentence $U_T(\ulcorner n \urcorner)$. This has no free variables because the term for $n$ has been substituted for the only free variable of $U_T(y)$.

It is true, separately, that the usual proof systems for first order logic do let you prove open sentences. It turns out that proving an open sentence is essentially the same as proving its universal closure. But this isn't really important for the case at hand, because the Gödel sentence doesn't have free variables.

-

You can indeed prove an open formula. For example, from $\forall x (x = x)$ you can deduce $x = x$. Although you can't assign the latter a truth-value in the same way which you can for the former, this is still a valid deduction. If you have some notes or text to reference, look at the rule for universal elimination, it will tell you precisely when you can eliminate a universal quantifier, and you'll see in particular that it allows you to deduce open formulas from closed sentences.

-
The poster is talking about formulas with free variables, which $\forall x(x=x)$ is not an example of. Rather, the formula $x=x$ is a formula with a free variable. In your express, $x$ is bound. –  Thomas Andrews Apr 24 '11 at 22:37
@Thomas: I believe Amit is saying that we can prove "x=x", which does have a free variable (of course). –  Carl Mummert Apr 24 '11 at 22:58
Some authors (e.g. Enderton) define an interpretation in such a way that it does assign truth values to all formulas, regardless whether they have free variables. In that convention, the truth values of open formulas are defined exactly the same way as the truth values of other formulas (using the same T-schema). –  Carl Mummert Apr 24 '11 at 23:14
Thanks for the help, Carl and Amit. I appreciate the point that the Godel sentence has no free variables (I tried to say that in my muddled original question), but I was missing the idea that open sentences can be proved from universal elimination. –  MBP Apr 27 '11 at 2:03