3 ms·
> given any formal system F that we might want to take as a foundation for mathematics (for example, Peano Arithmetic or Zermelo-Fraenkel set theory), Gödel tel
by radarsat1 15y ago
> given any formal system F that we might want to take as a foundation for mathematics (for example, Peano Arithmetic or Zermelo-Fraenkel set theory), Gödel tells us that there are Turing machines that run forever, but that can’t be proved to run forever in F.
Wow. I've never understood Godel's theorem before. I've never seen it put that way. Thank you! Is Godel's incompleteness theorem effectively the same thing as the halting problem then? Or rather, a result of it?
- smanek 15y agoThe halting problem is a specific instance of the type of problems predicted by the incompleteness theorem (IT). The first IT says there within any system of logic that's powerful enough to express arithmetic (and consistent), there are always statements that are true that can't be proved true. A specific program, P, that doesn't halt, but can't be proved not to halt, is an example of this. (Or, more precisely, the statement 'The program P halts' is the example.) The second IT says you can't prove the consistency of a system from within that system itself, but that's another story.
- radarsat1 15y agoOkay, so then you can't say from some point of view that IT is a _result_ of the halting problem, right? It's only the other way around?