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):


*

*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." 

*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.
 A: 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.
A: 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. 
