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.