4 ms·

What I don't get about Goedel's Incompleteness Theorem is why it's considered a problem in the general sense. It shows that in any formal system (of sufficient

by Tycho 13y ago

What I don't get about Goedel's Incompleteness Theorem is why it's considered a problem in the general sense. It shows that in any formal system (of sufficient power etc. etc.) you can produce a Goedel number which cannot be interpreted via the system as both provable and true at the same time. So in the strictest sense the system cannot be complete... but have we shown that it is missing anything except these incredibly tortuous, specific Goedel numbers? Isn't it a bit of a dead end? (happy to be corrected on this)

cousin_it 13y ago
If Peano arithmetic (PA) is consistent, the following statements are true but not provable in PA: 1) Consistency of PA 2) http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theore... 3) http://en.wikipedia.org/wiki/Goodstein%27s_theorem http://en.wikipedia.org/wiki/Goodstein%27s_theorem
- cwzwarich 13y ago
  But that's not much of a practical problem, since ZF set theory proves them both.
  - wfn 13y ago
    Ah, but the consistency of ZFC itself is undecidable from within ZFC! [1] I see what you're saying; it's quite the rabbit hole, however. [1]: https://en.wikipedia.org/wiki/List_of_statements_undecidable_in_ZFC https://en.wikipedia.org/wiki/List_of_statements_undecidable...
jerf 13y ago
It's easier to answer that question about the Halting Problem, so here's Scott Aaronson proving it as a corollary to the Halting Problem: http://www.scottaaronson.com/blog/?p=710 http://www.scottaaronson.com/blog/?p=710 Then, defending the value of the Halting Problem as a real problem is easy, relatively generally through Rice's Theorem: http://en.wikipedia.org/wiki/Rice%27s_theorem http://en.wikipedia.org/wiki/Rice%27s_theorem In colloquial terms, one can render Rice's Theorem as "Would you like to produce a program that can prove anything remotely interesting across the set of all possible inputs? TOO BAD!" That's glib, but less inaccurate than we'd like. Godel's theorem is, as Scott said, really sort of ad hoc and hard to easily apply in your head the way you're asking about. The Halting Problem, on the other hand, turns up everywhere, in real life (though many people still often don't realize it).
- PeterisP 13y ago
  My personal pet peeve is the Halting problem - yes, we can't prove interesting things for 'set of all possible inputs'. However, my [unverified] gut feeling is that we can prove halting/nonhalting (via static analysis and restricting types of code that are allowed) for the large class of things that we actually use (or should use) in practice and vice versa - we should push the convoluted cases (where analysis isn't possible) away from practical usage, since if a well-designed computer system can't reason about them, then likely the programmer can't as well and that part is buggy in some corner case. I.e., if your webservice isn't provably halting, guaranteeing a return value within a (short) bounded time - then it's too complex and is 99.9% likely to have a security flaw that allows denial of service or execution of arbitrary code in which case, naturally, you can't reason about it as the halting theorem proves. We don't even need to know a "proper" answer to the halting question - guaranteed to finish under X steps/whatever: okay; not guaranteed (maybe halting in X+1 steps): suspect/bad. That would be good enough for practical purposes in most systems.
  - munin 13y ago
    you're right. you can also soundly construct an analysis that asks "is this program safe" and answers with one of {yes, no, maybe I don't know}. and then, you interpret a result of "no" and "maybe I don't know" to mean the same thing and re-write the program until you get a "yes"...
  - ElectroPrime 13y ago
    Keep in mind that real world computers just have a very large (but not unbounded) amount of tape. Since they have constant space, they are really just DFAs.
    - jronkone 13y ago
      Does taking input from the outside (e.g. internet) change this?
  - jerf 13y ago
    It is unclear to me whether you are advocating for a programming style that you think is desirable but nonexistent, or if you're advocating for a programming style without naming it. If the former, you should know you are not alone and serious attempts to create such programming languages are afoot. It's hard for me to find any solid, single web page to point you at, but you want to look at the more theoretical end of Haskell, and Agda and Coq, for some examples. Interesting Google terms include "structural recursion" and various other recursion schemes, and also things like http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html .
joe_the_user 13y ago
You are correct that Goedel really isn't hard. And, of course, its not a problem but a theory. The thing is Goedel shaped the development of logic itself tremendously. Before Goedel, the idea was that proven theorems were essentially the true theorems. The concept of theory proving as a simply mechanical process wasn't there, the idea of models and true-but-not-provable theories wasn't there etc. Contrawise, once you have this machinery, the theorem is fairly simple (if sometimes tedious) to produce. So sketching Goedel's theorem can't help but be sketching early twentieth century logic.

by Tycho 13y ago

cousin_it 13y ago

If Peano arithmetic (PA) is consistent, the following statements are true but not provable in PA: 1) Consistency of PA 2) http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theore... 3) http://en.wikipedia.org/wiki/Goodstein%27s_theorem http://en.wikipedia.org/wiki/Goodstein%27s_theorem

cwzwarich 13y ago
But that's not much of a practical problem, since ZF set theory proves them both.
- wfn 13y ago
  Ah, but the consistency of ZFC itself is undecidable from within ZFC! [1] I see what you're saying; it's quite the rabbit hole, however. [1]: https://en.wikipedia.org/wiki/List_of_statements_undecidable_in_ZFC https://en.wikipedia.org/wiki/List_of_statements_undecidable...

jerf 13y ago

It's easier to answer that question about the Halting Problem, so here's Scott Aaronson proving it as a corollary to the Halting Problem: http://www.scottaaronson.com/blog/?p=710 http://www.scottaaronson.com/blog/?p=710 Then, defending the value of the Halting Problem as a real problem is easy, relatively generally through Rice's Theorem: http://en.wikipedia.org/wiki/Rice%27s_theorem http://en.wikipedia.org/wiki/Rice%27s_theorem In colloquial terms, one can render Rice's Theorem as "Would you like to produce a program that can prove anything remotely interesting across the set of all possible inputs? TOO BAD!" That's glib, but less inaccurate than we'd like. Godel's theorem is, as Scott said, really sort of ad hoc and hard to easily apply in your head the way you're asking about. The Halting Problem, on the other hand, turns up everywhere, in real life (though many people still often don't realize it).

PeterisP 13y ago
My personal pet peeve is the Halting problem - yes, we can't prove interesting things for 'set of all possible inputs'. However, my [unverified] gut feeling is that we can prove halting/nonhalting (via static analysis and restricting types of code that are allowed) for the large class of things that we actually use (or should use) in practice and vice versa - we should push the convoluted cases (where analysis isn't possible) away from practical usage, since if a well-designed computer system can't reason about them, then likely the programmer can't as well and that part is buggy in some corner case. I.e., if your webservice isn't provably halting, guaranteeing a return value within a (short) bounded time - then it's too complex and is 99.9% likely to have a security flaw that allows denial of service or execution of arbitrary code in which case, naturally, you can't reason about it as the halting theorem proves. We don't even need to know a "proper" answer to the halting question - guaranteed to finish under X steps/whatever: okay; not guaranteed (maybe halting in X+1 steps): suspect/bad. That would be good enough for practical purposes in most systems.
- munin 13y ago
  you're right. you can also soundly construct an analysis that asks "is this program safe" and answers with one of {yes, no, maybe I don't know}. and then, you interpret a result of "no" and "maybe I don't know" to mean the same thing and re-write the program until you get a "yes"...
- ElectroPrime 13y ago
  Keep in mind that real world computers just have a very large (but not unbounded) amount of tape. Since they have constant space, they are really just DFAs.
  - jronkone 13y ago
    Does taking input from the outside (e.g. internet) change this?
- jerf 13y ago
  It is unclear to me whether you are advocating for a programming style that you think is desirable but nonexistent, or if you're advocating for a programming style without naming it. If the former, you should know you are not alone and serious attempts to create such programming languages are afoot. It's hard for me to find any solid, single web page to point you at, but you want to look at the more theoretical end of Haskell, and Agda and Coq, for some examples. Interesting Google terms include "structural recursion" and various other recursion schemes, and also things like http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html .

joe_the_user 13y ago

You are correct that Goedel really isn't hard. And, of course, its not a problem but a theory. The thing is Goedel shaped the development of logic itself tremendously. Before Goedel, the idea was that proven theorems were essentially the true theorems. The concept of theory proving as a simply mechanical process wasn't there, the idea of models and true-but-not-provable theories wasn't there etc. Contrawise, once you have this machinery, the theorem is fairly simple (if sometimes tedious) to produce. So sketching Goedel's theorem can't help but be sketching early twentieth century logic.