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 proo

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.