|
|
|
|
|
|
by jleader
3761 days 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! |
|
|
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.