[repsilat]

He's not assuming finiteness, just countability.

An example of how this is useful: If it were provable that a program does not halt, an enumeration of all proofs would find the proof that the program does not halt. (If a program does halt, it is necessarily provable that it does so, for obvious reasons.)

Thus either,

- We can solve the halting problem, or - There exists something that is true but not provable.

Thus the uncomputability of the halting problem implied Goedel's incompleteness theorem. Proving the other direction can be done by similar techniques.