7 ms·
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 syst
by jleader 11y ago
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!
- repsilat 11y agoHe'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.