8 ms·

Cool page, though the Halting Problem brings with it a lot of stuff, so using it to prove Godel's first incompleteness theorem is (imo) a bit like cheating. I'v

by dvt 4y ago

Cool page, though the Halting Problem brings with it a lot of stuff, so using it to prove Godel's first incompleteness theorem is (imo) a bit like cheating. I've proven it before using diagonalization on my blog (but also using concepts like computability for free). At the end of the day, using these ideas, you get the Curry–Howard correspondence for free (which, again, is a bit like cheating). > Gödel’s original proof was slightly stronger Technically speaking, a lot stronger. Proving Godel's first incompleteness theorem (don't even get me started on the second) from first principles is actually much more involved; and certainly more difficult to make it intelligible for non-logicians.

whimsicalism 4y ago
If you've managed to prove the halting problem, then I don't think it is cheating to use it on an easier result. This is how it was taught when I learned CS theory in uni [0] [0]: https://introtcs.org/public/lec_09_godel.html https://introtcs.org/public/lec_09_godel.html
- ianai 4y ago
  Further, there just isn’t “cheating” in a proof. Being able to do a demonstration yet another way just illuminates the phenomena all the better. You might know something if you know one way to do it. You have a much better understanding if you have two ways. Three and your understanding is probably pretty solid. Etc Edit of to if, damn autocorrect
Grothendank 4y ago
IMO It's cool to invoke the lean halting theorem, since the author proves the informal version of the halting theorem in the previous lesson. See: https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem
fithisux 4y ago
Where is your blog?
- alberto_ol 4y ago
  https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers/ https://dvt.name/2018/03/12/godels-first-incompleteness-theo...
lapcat 4y ago
> Proving Godel's first incompleteness theorem (don't even get me started on the second) from first principles is actually much more involved; and certainly more difficult to make it intelligible for non-logicians. I remember having to do it for my logic class final exam. I wouldn't remember exactly how to do it today though. The little click sounds on the linked page are unfortunate. I had to stop after like 20 seconds.
deleted 4y ago
[deleted]
lisper 4y ago
> the Halting Problem brings with it a lot of stuff Not really. The idea of a Turing Machine brings with it a lot of stuff, but nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place. So proving the non-computability of the halting problem is pretty easy [1]: Assume that there exists a program H that solves the halting problem, that is, H takes two input parameters, a program P and an input I and returns true if P halts when run on input I, false otherwise. Construct a program B that does the following: B accepts as input a program P and computes H(P,P), that is, it calls H as a subroutine to determine if program P halts when run on a copy of itself as the input. If the result from H is true then B enters an infinite loop, otherwise B halts (that is, B does the opposite of what P would do when run on a copy of itself). Now consider what happens if we run B on a copy of itself. B will halt iff H(B,B) is false. But H(B,B) is false iff B doesn't halt, which is a contradiction. Therefore, our assumption is false, and H is impossible. QED. --- [1] Taken from https://flownet.com/ron/chaitin.html https://flownet.com/ron/chaitin.html
- dvt 4y ago
  > nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place I think you may have misconstrued what I meant. From a metamathematical standpoint, leveraging the Halting Problem gives you a lot of stuff for free. Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Specifically, Godel numbering really originally made this entire thing work. And that sausage was not very intuitively-made.
  - lisper 4y ago
    > leveraging the Halting Problem gives you a lot of stuff for free. Not exactly for free. You still have to prove the non-computability of the halting problem. But I get your meaning. > Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Sure, but that is no different from any technological advance. Arabic numerals were a major breakthrough when they were first invented. Nowadays it is pretty safe to take them for granted in most cases. > Godel numbering really originally made this entire thing work. Sure, but that was only necessary because Godel didn't know about ASCII. Proving Godel's theorem using Godel numbers is kind of like writing a C compiler as a state table for a Turing Machine. You could do it, but no one in their right mind would except perhaps as an intellectual exercise. The history of how technological innovations came about is very different, and usually much more difficult, than the way one can re-invent those innovations with the benefit of hindsight.

by dvt 4y ago

whimsicalism 4y ago

If you've managed to prove the halting problem, then I don't think it is cheating to use it on an easier result. This is how it was taught when I learned CS theory in uni [0] [0]: https://introtcs.org/public/lec_09_godel.html https://introtcs.org/public/lec_09_godel.html

ianai 4y ago
Further, there just isn’t “cheating” in a proof. Being able to do a demonstration yet another way just illuminates the phenomena all the better. You might know something if you know one way to do it. You have a much better understanding if you have two ways. Three and your understanding is probably pretty solid. Etc Edit of to if, damn autocorrect

Grothendank 4y ago

IMO It's cool to invoke the lean halting theorem, since the author proves the informal version of the halting theorem in the previous lesson. See: https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem

fithisux 4y ago

Where is your blog?

alberto_ol 4y ago
https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers/ https://dvt.name/2018/03/12/godels-first-incompleteness-theo...

lapcat 4y ago

> Proving Godel's first incompleteness theorem (don't even get me started on the second) from first principles is actually much more involved; and certainly more difficult to make it intelligible for non-logicians. I remember having to do it for my logic class final exam. I wouldn't remember exactly how to do it today though. The little click sounds on the linked page are unfortunate. I had to stop after like 20 seconds.

deleted 4y ago

[deleted]

lisper 4y ago

> the Halting Problem brings with it a lot of stuff Not really. The idea of a Turing Machine brings with it a lot of stuff, but nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place. So proving the non-computability of the halting problem is pretty easy [1]: Assume that there exists a program H that solves the halting problem, that is, H takes two input parameters, a program P and an input I and returns true if P halts when run on input I, false otherwise. Construct a program B that does the following: B accepts as input a program P and computes H(P,P), that is, it calls H as a subroutine to determine if program P halts when run on a copy of itself as the input. If the result from H is true then B enters an infinite loop, otherwise B halts (that is, B does the opposite of what P would do when run on a copy of itself). Now consider what happens if we run B on a copy of itself. B will halt iff H(B,B) is false. But H(B,B) is false iff B doesn't halt, which is a contradiction. Therefore, our assumption is false, and H is impossible. QED. --- [1] Taken from https://flownet.com/ron/chaitin.html https://flownet.com/ron/chaitin.html

dvt 4y ago
> nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place I think you may have misconstrued what I meant. From a metamathematical standpoint, leveraging the Halting Problem gives you a lot of stuff for free. Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Specifically, Godel numbering really originally made this entire thing work. And that sausage was not very intuitively-made.
- lisper 4y ago
  > leveraging the Halting Problem gives you a lot of stuff for free. Not exactly for free. You still have to prove the non-computability of the halting problem. But I get your meaning. > Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians. Sure, but that is no different from any technological advance. Arabic numerals were a major breakthrough when they were first invented. Nowadays it is pretty safe to take them for granted in most cases. > Godel numbering really originally made this entire thing work. Sure, but that was only necessary because Godel didn't know about ASCII. Proving Godel's theorem using Godel numbers is kind of like writing a C compiler as a state table for a Turing Machine. You could do it, but no one in their right mind would except perhaps as an intellectual exercise. The history of how technological innovations came about is very different, and usually much more difficult, than the way one can re-invent those innovations with the benefit of hindsight.