upvote
The undecidability of the halting problem yields an easy proof of Gödel's "zeroth" incompleteness theorem:

Statement: Every sound (i.e. not just consistent, but sound) recursive theory of arithmetic is incomplete.

Proof: Assume it is complete. List all its theorems by a program. Then one can decide the halting problem as follows: for any instance, look whether "the program halts" or "the program does not halt" shows up in the list of theorems (since the theory is complete, one of them must show up; and since the theory is sound, the theorem is true).

reply
Right, if you're a software engineer, the realization that the two theorems are nearly-equivalent really takes the air out of a lot of the existential philosophizing around Gödel's incompleteness.

Gödel's argument basically says that any system of mathematics powerful enough to implement basic arithmetic is a computer. This shouldn't be surprising to software engineers because the equivalency between Boolean logic and arithmetic is easy to show. And if you have a computer, you can build algorithms whose outcome can't be programmatically decided by other algorithms.

reply
I think that's selling the theorems a little short. A math system with arithmetic is equal to, or more powerful than, a computer. For an example, even classical logic comes with the law of excluded middle that can say (internally) if a program halts or not. Incompleteness applies to all the stronger systems as well.
reply
[dead]
reply
Also check out https://en.wikipedia.org/wiki/Rice%27s_theorem

basically generalized the halting problem to arbitrary semantic properties.

reply
It's convenient that Henry Rice lived long before the age of language cults. I don't even think Rice wrote software, he's just a mathematician, he proved this nice property in mathematics. Stuff like FORTRAN and ALGOL happens later.

Also though, just as for the Halting Problem, we are always allowed a three-way split. Rice proves that "Has property" vs "Does not have property" can't be done, but "Has property" vs "Does not have property" vs "Shrug - I dunno, seems hard" is possible, and indeed easy if you're OK with lots of machines landing in the "Shrug" pile. You can expend as much work as you like to shrink that pile, Rice just proved it would need infinite work to empty it completely.

reply
Another way around the Rice's theorem is the Curry-Howard correspondence. A constructive proof of existence of a program that has a property can be transformed into a program that has this property. Yet another way is to have a programming language where syntactic correctness implies a range of semantic properties.
reply
Halting problem concerns decidability, not completeness
reply
Sure but that's fairly pedantic. You can derive Godel's first incompleteness theorems strictly as a consequence of undecidability of the halting problem.
reply