He&#x27;s not assuming finiteness, just countability.<p>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 <i>does</i> halt, it is necessarily provable that it does so, for obvious reasons.)<p>Thus either,<p>- We can solve the halting problem, or
 - There exists something that is true but not provable.<p>Thus the uncomputability of the halting problem implied Goedel&#x27;s incompleteness theorem. Proving the other direction can be done by similar techniques.