Goedel's proof



Let me see if I understand Goedel's proof correctly.

Let's list all the formulas of first order logic with one free variable
in some order:

f1(n)
f2(n)
f3(n)
f4(n)
f5(n)

We can replace the free variable with integers

f1(1) f1(2) f1(3) f1(4) f1(5) ... f1(q)
f2(1) f2(2) f2(3) f2(4) f2(5) ... f2(q)
f3(1) f3(2) f3(3) f3(4) f3(5) ... f3(q)
f4(1) f4(2) f4(3) f4(4) f4(5) ... f4(q)
f5(1) f5(2) f5(3) f5(4) f5(5) ... f5(q)
.......................................
.......................................
fq(1) fq(2) fq(3) fq(4) fq(5) ... fq(q)

We will now focus on the wffs on the diagonal
f1(1), f2(2), f3(3), f4(4), f5(5), ...
It turns out that we can define a formula that states that none of the
above is provable. Let fq(n) be this formula

fq(1) == f1(1) is not provable
fq(2) == f2(2) is not provable
fq(3) == f3(3) is not provable
fq(4) == f4(4) is not provable
fq(5) == f5(5) is not provable
...............................................
...............................................
fq(q) == fq(q) is not provable
It follows that fq(q) is undecidable blah blah blah.

.