|
That statement is too strong. The practical effect is that you should not try to build an algorithm to detect infinite loops in general (though you wouldn't need undecidability for this, per se. E.g., NP-completeness of the halting problem would probably have been sufficient to kill attempts at a general algorithm dead in the water). Of course, it is true in specific cases that you can decide whether a given program halts, and, indeed in almost all practical instances if you know how to solve a given problem then you should be able to construct an algorithm to solve it which provably halts. (Not including, of course, things that depend on environmental inputs, something that computes whether a given number satisfies Goldbach's conjecture, etc.) There is, of course, enormous theoretical value in the undecidability of the halting problem, and in Kurt Gödel's undecidability of a general axiomatic system. And this theoretical value guides future theoretical research which is likely to lead to further practical value in future - which indicates a practical effect in the long-term. Also, of course, it indicates that an attempt to build a general theorem-prover is a useless endeavor (though approximate / specialized theorem provers are, of course, possible and indeed exist). In particular, Gödel's undecidability has quite real implications for an Artificial General Intelligence which would have to reason about mathematics in general, and about its own thought processes in particular. Under classical mathematical reasoning, such an AI would be unable to "have confidence" in its own reasoning process. However, if the assumptions are relaxed from statements with 0/1 truth values to statements with probabilities, and time-independence of truth is relaxed, it is possible to define an agent which is able to assign (almost) consistent (actually "coherent") probabilities to what its own beliefs w̶i̶l̶l̶ ̶b̶e̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶m̶i̶t̶ ̶(̶a̶s̶ ̶t̶ ̶g̶o̶e̶s̶ ̶t̶o̶ ̶i̶n̶f̶i̶n̶i̶t̶y̶)̶) are at time t. See https://arxiv.org/abs/1609.03543 for more details. This is probably the strongest such statement that can be made in this class of arguments. |