The author keeps talking about going through all possible proofs built from the axioms, as if that&#x27;s a thing that obviously could be done. However, if your system is complicated enough to allow arbitrarily large combinations of axioms in your proofs, then I don&#x27;t understand how you can expect enumeration of all proofs to be a finite process. Any statement that says &quot;enumerate all possible proofs&quot; followed by &quot;and then do X&quot; is meaningless, because you will never reach the &quot;do X&quot; step!