Comment by jleader

The author keeps talking about going through all possible proofs built from the axioms, as if that'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't understand how you can expect enumeration of all proofs to be a finite process. Any statement that says "enumerate all possible proofs" followed by "and then do X" is meaningless, because you will never reach the "do X" step!