Hacker News Reader

Comment by Tycho | Hacker News Reader

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)

View on HN

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

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

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

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.

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

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.

Does taking input from the outside (e.g. internet) change this?

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 .

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

3) http://en.wikipedia.org/wiki/Goodstein%27s_theorem

But that's not much of a practical problem, since ZF set theory proves them both.

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

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.

Reply on news.ycombinator.com