How is a Godel sentence constructed?

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.