5 ms·

Of all the incompleteness-style theorems, I find the Halting problem to be the most approachable and also the most interesting. Maybe it's because I'm a softwar

Of all the incompleteness-style theorems, I find the Halting problem to be the most approachable and also the most interesting. Maybe it's because I'm a software dev that dabbles in math rather than the other way around. But that makes me wonder if all of Gödel's theorems can be stated if 'software form', so to speak.

lacewing 4mo ago
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.
- mspn 4mo ago
  [dead]
- cobbal 4mo ago
  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.
  - voxl 4mo ago
    There is no logic that is more expressive than a Turing machine. In fact, just about every logic you know can only expressive necessarily terminating programs. There is a bit of an issue on what exactly someone means by expressive, but if we're talking programs that compute outputs from inputs (without caring about the invariants imposed on said programs) then this holds.
olmo23 4mo ago
Also check out https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem basically generalized the halting problem to arbitrary semantic properties.
- tialaramex 4mo ago
  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.
  - red75prime 4mo ago
    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.
oulipo2 4mo ago
Halting problem concerns decidability, not completeness
- Maxatar 4mo ago
  Sure but that's fairly pedantic. You can derive Godel's first incompleteness theorems strictly as a consequence of undecidability of the halting problem.
bananaflag 4mo ago
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).
- jojomodding 4mo ago
  This also makes it obvious that at some point, the halting problem becomes "unprovably hard." There must be Turing Machines for which it is independent of the accepted axioms of mathematics whether or not they halt. And indeed, constructing such machines is not too difficult. There is current research into finding the smallest such Turing Machine. Here is one with 748 states: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...
cyberax 4mo ago
The proof of the first incompleteness theorem is a very technical way of constructing the statement: "The truth of this statement is unproveable". In the software form, it can be restated as: "there is no finite program that outputs the sequence with this property".

lacewing 4mo ago

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.

mspn 4mo ago
[dead]
cobbal 4mo ago
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.
- voxl 4mo ago
  There is no logic that is more expressive than a Turing machine. In fact, just about every logic you know can only expressive necessarily terminating programs. There is a bit of an issue on what exactly someone means by expressive, but if we're talking programs that compute outputs from inputs (without caring about the invariants imposed on said programs) then this holds.

olmo23 4mo ago

Also check out https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem basically generalized the halting problem to arbitrary semantic properties.

tialaramex 4mo ago
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.
- red75prime 4mo ago
  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.

oulipo2 4mo ago

Halting problem concerns decidability, not completeness

Maxatar 4mo ago
Sure but that's fairly pedantic. You can derive Godel's first incompleteness theorems strictly as a consequence of undecidability of the halting problem.

bananaflag 4mo ago

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).

jojomodding 4mo ago
This also makes it obvious that at some point, the halting problem becomes "unprovably hard." There must be Turing Machines for which it is independent of the accepted axioms of mathematics whether or not they halt. And indeed, constructing such machines is not too difficult. There is current research into finding the smallest such Turing Machine. Here is one with 748 states: https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-undecidability-bb748.pdf https://www.ingo-blechschmidt.eu/assets/bachelor-thesis-unde...

cyberax 4mo ago

The proof of the first incompleteness theorem is a very technical way of constructing the statement: "The truth of this statement is unproveable". In the software form, it can be restated as: "there is no finite program that outputs the sequence with this property".