10 ms·

Does anyone have a better metaphor, or a link to someplace with a better explanation, of the Incompleteness Theorem?

beaconstudios 8y ago
I'm not familiar with directly, but if you're more familiar with comp-sci: based on my understanding of Curry-Howard correspondence, I would think it's the logic equivalent of the halting problem. I could be way off-base though, I'd appreciate a mathematician chiming in on whether my intuition is accurate here.
- chriswarbo 8y ago
  (Caveat: I'm a computer scientist, not a mathematician) The halting problem, and universal computation itself, came directly out of work on incompleteness. Incompleteness is about being unable to prove statements in a particular system; it leaves open the possibility that a more powerful system might be able to prove that statement (but that more powerful system will have its own incompleteness, and so on). Turing got involved after attending a series of lectures on Goedel's incompeteness theorem. He came up with turing machines, showed that they cannot decide their own halting problem, and proved that they're equivalent to lambda calculus. Goedel tried to make a more powerful alternative to lambda calculus, called general recursive functions, but it also turned out to be equivalent to turing machines and lambda calculus. This lead to the Church-Turing thesis, which claims that any effective/physical/realisable system of logic cannot be more powerful than turing machines/lambda calculus/general recursive functions. In this sense, we can still "solve" the halting problem by using a more powerful logical system (e.g. oracle machines), but the Church Turing thesis says that we can never carry out those calculation to get a true/false answer. I like to think of incompleteness as a mathematical property, applying to all systems but allowing the "escape hatch" of switching to a more powerful system; and I like to think of the Church Turing thesis as a law of physics, that there is a limit to the logical power of any physical system (i.e. Turing completeness). There's a nice summary at https://www.youtube.com/watch?v=GnpcMCW0RUA https://www.youtube.com/watch?v=GnpcMCW0RUA
  - beaconstudios 8y ago
    the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there.
    - lisper 8y ago
      > what is the property of a program that makes it undecidable? That is itself an undecidable question! There are a lot of programs for which you can tell that they halt (programs with no loops, for example). Likewise there are a lot of programs for which you can tell that they do not halt (any program whose main body is a WHILE TRUE loop in a language that does not have exceptions, for example.) And then there are lots of more complicated cases for which the answer can be found. But there are some cases where we just don't know. The best known is this: https://en.wikipedia.org/wiki/Collatz_conjecture https://en.wikipedia.org/wiki/Collatz_conjecture Not only do we not know the answer, but we don't know if it is even possible to find the answer! We know (because Turing) that there exist programs for which we cannot find the answer, but we don't know whether the Collatz problem is one of them. And in general we cannot know, because if we could then we could use that knowledge to solve the halting problem itself! (We might be able to prove undecidability for particular programs, just as we can prove halting or non-halting for particular programs, but deciding undecidability for any particular program is in general undecidable!)
      - beaconstudios 8y ago
        but that's exactly my point - there are clear-cut halting, clear-cut non-halting, and "we don't know yet" programs. My interest is in delineating the properties that separate the 3. The collatz conjecture is exactly the example I use when explaining the "we don't know yet" programs. If I could build a logic system that can positively prove halting, and one that can positively prove non-halting, then anything that remains is "dunno". The halting problem is basically showing that you can never prove the category of "dunno" to be empty. Which is pretty self-evident given there are unsolved bounding problems like the collatz conjecture in mathematics. For a minimal example, if I create a program that takes an AST and runs it through two truth functions, one that checks if the AST === "return;" and prints "it halts" and one that checks if the AST === "while(true) {}" and prints "it never halts", then we've already created such an application, just with a "dunno" space containing the majority of programs. Adding practical axioms to a logic system could grow the "halts" and "never halts" spaces to the point where only a subset of applications cannot be excluded from the "dunno" space, and my question is: what are the unique properties of those applications?
fifticon 8y ago
It proves, that it is impossible to design any formal system, within which it would be possible to prove every principle/aspect that applied to that same system ( aspects that nevertheless WERE true, and CAN be proven by using a 'bigger hammer'.) In a way, the problem is, that whenever you expand your system to make it 'more complete' (to be able to prove more stuff), you'll invariably introduce new aspects you THEN can't cover. You "can't pull yourself up by your own hair".
stuntkite 8y ago
Here's a pretty good reddit discussion about it. That's the best I could find with a quick google. https://www.reddit.com/r/rational/comments/30144c/geb_discussion_4_chapter_3_figure_and_ground/ https://www.reddit.com/r/rational/comments/30144c/geb_discus...
pvg 8y ago
https://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/08147583... Can be read in a couple of hours and you'll know as much about Goedel's work as any GEB reader. Nowadays even comes with a Hofstadter intro but no bulk or talking animals.
lisper 8y ago
Excerpted from http://www.flownet.com/ron/chaitin.html http://www.flownet.com/ron/chaitin.html: Proof of the undecidability of the halting problem in six sentences: 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. Turing's original proof of this theorem was remarkable (and complicated) because in his day there were no computers. Not only did Turing have to more or less invent the idea of a program, but he had to conceive of the rather mind-bending idea of running a program with a copy of itself as input. Nowadays this is commonplace. The unix command "cat `which cat`" is one of the simplest examples of a program operating on itself as input. A compiler that compiles itself is another.
ufo 8y ago
The incompleteness theorem says that if your logical system is powerful enough to describe the natural numbers (Peano's axioms) then it is also powerful enough to write down self referential paradoxes, like "this theorem cannot be proved". This means that your system either is unsound (if you can prove the paradoxical sentence then you are simultaneously proving it to be true and false) or that it is incomplete (some sentences, including the paradoxical ones, cannot be proved). You can't be sound and complete at the same time in the presence of self-referential paradoxes. The proof of Godel's theorem involves showing that you can encode theorems and their proofs using just integer arithmetic. For example, you can use tricks like encoding the string "ab" as 2ᵃ3ᵇ. The incompleteness theorem is very closely related to Turing's undecidability theorem, which shows that by encoding programs as strings and passing them as inputs to other programs you can create paradoxical self-referential problem statements that no program can solve in finite time. It also reminds me of the lambda calculus, which is something that really shows how far you can go by starting out with a barebones system and encoding everything else on top of it. The lambda calculus starts with only anonmour functions and is able to encode numbers, arithmetic, data structures, iteration and everything else with just that. Godel's theorem uses similar tricks to show that if you start with just integer arithmetic you can also go all the way to "turing completeness".

I'm not familiar with directly, but if you're more familiar with comp-sci: based on my understanding of Curry-Howard correspondence, I would think it's the logic equivalent of the halting problem. I could be way off-base though, I'd appreciate a mathematician chiming in on whether my intuition is accurate here.

chriswarbo 8y ago
(Caveat: I'm a computer scientist, not a mathematician) The halting problem, and universal computation itself, came directly out of work on incompleteness. Incompleteness is about being unable to prove statements in a particular system; it leaves open the possibility that a more powerful system might be able to prove that statement (but that more powerful system will have its own incompleteness, and so on). Turing got involved after attending a series of lectures on Goedel's incompeteness theorem. He came up with turing machines, showed that they cannot decide their own halting problem, and proved that they're equivalent to lambda calculus. Goedel tried to make a more powerful alternative to lambda calculus, called general recursive functions, but it also turned out to be equivalent to turing machines and lambda calculus. This lead to the Church-Turing thesis, which claims that any effective/physical/realisable system of logic cannot be more powerful than turing machines/lambda calculus/general recursive functions. In this sense, we can still "solve" the halting problem by using a more powerful logical system (e.g. oracle machines), but the Church Turing thesis says that we can never carry out those calculation to get a true/false answer. I like to think of incompleteness as a mathematical property, applying to all systems but allowing the "escape hatch" of switching to a more powerful system; and I like to think of the Church Turing thesis as a law of physics, that there is a limit to the logical power of any physical system (i.e. Turing completeness). There's a nice summary at https://www.youtube.com/watch?v=GnpcMCW0RUA https://www.youtube.com/watch?v=GnpcMCW0RUA
- beaconstudios 8y ago
  the question that fascinates me is - what is the property of a program that makes it undecidable? I've been playing around with the idea of trying to make a program that determines halts/doesn't halt/don't know, given some representation of a program. I'm running into some interesting implications when I incorporate dependent typing, but it feels like there must be something theoretical that's already out there.
  - lisper 8y ago
    > what is the property of a program that makes it undecidable? That is itself an undecidable question! There are a lot of programs for which you can tell that they halt (programs with no loops, for example). Likewise there are a lot of programs for which you can tell that they do not halt (any program whose main body is a WHILE TRUE loop in a language that does not have exceptions, for example.) And then there are lots of more complicated cases for which the answer can be found. But there are some cases where we just don't know. The best known is this: https://en.wikipedia.org/wiki/Collatz_conjecture https://en.wikipedia.org/wiki/Collatz_conjecture Not only do we not know the answer, but we don't know if it is even possible to find the answer! We know (because Turing) that there exist programs for which we cannot find the answer, but we don't know whether the Collatz problem is one of them. And in general we cannot know, because if we could then we could use that knowledge to solve the halting problem itself! (We might be able to prove undecidability for particular programs, just as we can prove halting or non-halting for particular programs, but deciding undecidability for any particular program is in general undecidable!)
    - beaconstudios 8y ago
      but that's exactly my point - there are clear-cut halting, clear-cut non-halting, and "we don't know yet" programs. My interest is in delineating the properties that separate the 3. The collatz conjecture is exactly the example I use when explaining the "we don't know yet" programs. If I could build a logic system that can positively prove halting, and one that can positively prove non-halting, then anything that remains is "dunno". The halting problem is basically showing that you can never prove the category of "dunno" to be empty. Which is pretty self-evident given there are unsolved bounding problems like the collatz conjecture in mathematics. For a minimal example, if I create a program that takes an AST and runs it through two truth functions, one that checks if the AST === "return;" and prints "it halts" and one that checks if the AST === "while(true) {}" and prints "it never halts", then we've already created such an application, just with a "dunno" space containing the majority of programs. Adding practical axioms to a logic system could grow the "halts" and "never halts" spaces to the point where only a subset of applications cannot be excluded from the "dunno" space, and my question is: what are the unique properties of those applications?

fifticon 8y ago

It proves, that it is impossible to design any formal system, within which it would be possible to prove every principle/aspect that applied to that same system ( aspects that nevertheless WERE true, and CAN be proven by using a 'bigger hammer'.) In a way, the problem is, that whenever you expand your system to make it 'more complete' (to be able to prove more stuff), you'll invariably introduce new aspects you THEN can't cover. You "can't pull yourself up by your own hair".

stuntkite 8y ago

Here's a pretty good reddit discussion about it. That's the best I could find with a quick google. https://www.reddit.com/r/rational/comments/30144c/geb_discussion_4_chapter_3_figure_and_ground/ https://www.reddit.com/r/rational/comments/30144c/geb_discus...

pvg 8y ago

https://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/Gödels-Proof-Ernest-Nagel/dp/08147583... Can be read in a couple of hours and you'll know as much about Goedel's work as any GEB reader. Nowadays even comes with a Hofstadter intro but no bulk or talking animals.

lisper 8y ago

Excerpted from http://www.flownet.com/ron/chaitin.html http://www.flownet.com/ron/chaitin.html: Proof of the undecidability of the halting problem in six sentences: 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. Turing's original proof of this theorem was remarkable (and complicated) because in his day there were no computers. Not only did Turing have to more or less invent the idea of a program, but he had to conceive of the rather mind-bending idea of running a program with a copy of itself as input. Nowadays this is commonplace. The unix command "cat `which cat`" is one of the simplest examples of a program operating on itself as input. A compiler that compiles itself is another.

ufo 8y ago

The incompleteness theorem says that if your logical system is powerful enough to describe the natural numbers (Peano's axioms) then it is also powerful enough to write down self referential paradoxes, like "this theorem cannot be proved". This means that your system either is unsound (if you can prove the paradoxical sentence then you are simultaneously proving it to be true and false) or that it is incomplete (some sentences, including the paradoxical ones, cannot be proved). You can't be sound and complete at the same time in the presence of self-referential paradoxes. The proof of Godel's theorem involves showing that you can encode theorems and their proofs using just integer arithmetic. For example, you can use tricks like encoding the string "ab" as 2ᵃ3ᵇ. The incompleteness theorem is very closely related to Turing's undecidability theorem, which shows that by encoding programs as strings and passing them as inputs to other programs you can create paradoxical self-referential problem statements that no program can solve in finite time. It also reminds me of the lambda calculus, which is something that really shows how far you can go by starting out with a barebones system and encoding everything else on top of it. The lambda calculus starts with only anonmour functions and is able to encode numbers, arithmetic, data structures, iteration and everything else with just that. Godel's theorem uses similar tricks to show that if you start with just integer arithmetic you can also go all the way to "turing completeness".