Gödel’s First Incompleteness Theorem for Programmers

https://dvt.name/2018/03/12/godels-first-incompleteness-theorem-programmers/

by dvt • 8 years ago

63 24 8 years ago

dvt.name

perfmode• 8 years ago

I love proofs of impossibility. Thanks for sharing

dvt7• 8 years ago

Thanks, I enjoyed writing it!

cousin_it• 8 years ago

The halting problem indeed proves easily that no theory can be complete and sound, but proving that no theory can be complete and consistent is a bit harder. More details here: https://www.scottaaronson.com/blog/?p=710

OtterCoder• 8 years ago

What's Q? They lost me there. A is all computable functions in... Something?

Also, if Turing completeness indicates that a language can simulate any mechanical process, and any Turing complete language must be Gödel incomplete, then that means there must be some physical facts that are simply inexpressible?

asynchrony• 8 years ago

Not inexpressible. Unprovable. There could be a set of correct programs that could never be proven correct by a type checker, for example.

dvt7• 8 years ago

Q is the set of all functions that take an integer as an input and return a 0 or a 1. A is the set of all function in Q that are computable.

davrosthedalek5• 8 years ago

Hmm, not sure I fully follow. I'll number my steps to help discussion:

1) The argument assumes that I can generate all programs and name them, right?

2)This indicates that there is a way to write a program in javascript which gives me f_i for i. Let's call that function gen_f(i)

3) Isn't the function fbar(i)=1-eval(gen_f(i))(i) a valid program? It obviously fulfills the premise.

4) The only way out here that I see is that gen_f is not halting, or that eval(gen_f(i)) is not halting.

5) The first case is possible, but then we can not generate the table, and without the table, it's not clear that fbar exists.

6) The second case means that we generated a non-halting function, i.e. f_i is not a computable function, and not part of F.

So, if we write a function gen_f, it's either not sound, as it gives functions which are actually not in F, or not complete, because it can then never give fbar. That's the trick, right?

dvt7• 8 years ago

2)This indicates that there is a way to write a program in javascript which gives me f_i for i. Let's call that function gen_f(i)

The whole point, actually, is that there isn't a way to write a program in JS which gives you f_i for i (pragmatically, you have no access to T). You might think of some clever way to try and augment your language (but that will be tricky; T is infinite but programs are finite, so you'll run into the Halting Problem). The Second Theorem of Incompleteness shows why you'll never be able to do that, but that's another post for another day.

davrosthedalek5• 8 years ago

I don't think T being infinite is a problem, you only need a cell, which is fin(it)e. But I don't like the argument with the halting problem: If you assume the halting problem as a given, it's trivial to show that there are uncomputable functions. Busy Beaver.

The halting problem follows from this automatically: The function gen_f cannot be correct and complete. On the other hand, if you could construct a function which solves the halting problem, you could, with that, construct gen_f to be correct and complete. So you cannot solve the halting problem.

Follow up question: Is the definition of T actually good enough? It's an infinite set, so are we sure that we can order the functions? Or do we need the axiom of choice somewhere?

wdrw• 8 years ago

f_i was defined as the ith program in lexicographical order that is guaranteed to terminate and to only return 0 or 1 (from the article: "we can just throw out programs that loop infinitely or don’t return a 1 or a 0")

This means that to write your "gen_f(i)" function, you'd have to solve the halting problem, which is impossible. So there is no mechanical (and hence no Javascript-based) way to create the gen_f(i) function.

Note that f_i is still a well-defined mathematical object, and so table T is a well-defined mathematical object (and then so is fbar). But they are not computable objects.

davrosthedalek5• 8 years ago

Well, f_i is certainly computable, because it's in A. I guess you mean f_bar? T is not computable, but T is also not a function out of F.

rrauenza• 8 years ago

This seems inspired by Cantor's infinity proof. I've seen a halting problem proof via Cantor's diagonal as well...

Are there any other significant proofs that use a similar methodology? Why does Cantor's method work well here? ...algorithms / programs are countably infinite, no?

(Finding this more interesting now than I did in school!)

pacifist• 8 years ago

Yes, Godel used Cantor's method of diagonalization in his proof. Turing also used it on the halting problem. Penrose talks about this in "The Emperor's New Mind." Cantor rocked the Casbah. Smart people saw it and used it.

dvt7• 8 years ago

Why does Cantor's method work well here? ...algorithms / programs are countably infinite, no?

It seems that A (computable functions that take an integer and return 0 or 1) are countably infinite but Q (all functions that take an integer and return 0 or 1) are uncountably infinite. As it turns out, there's a lot more stuff that we can't prove than stuff we can.

kalkut• 8 years ago

It is cool to see that expressing mathematical proofs with programming concepts/tool/languages is that efficient. I already was taught the Cantor proof but I feel more confident in my ability to explain this variation to a co-worker with no maths background.

Non-CS maths are too rarely taught the CS way.

dvt7• 8 years ago

Thanks! Glad you enjoyed it.

invincing2• 8 years ago

Late to the party, but the proof requires integers with infinite amount of bits. With real-life programming languages there's limited number of bits in integers, and this means that the proof doesn't work with any real-life language such as Javascript.

Consider just 2-bit integers (because it makes this easy, in real life the number of bits is of course larger). If i in F(i) has just 2 bits (possible values thus are 0,1,2,3), each Fn(i) can be represented by a table of four 0/1 values. The function just returns the value at the table in the input index. This also means that there are only 16 possible functions Fn() for a 2-bit input (as return values 0 and 1 can be combined in 16 ways in the 4-entry table). There may be infinite amount of lexically different functions, but based on what the functions actually do, most of them are duplicates that provide the same functionality.

All possible functions with 2-bit input value, and their respective 1-bit return values can be written out to a table: input: 0 1 2 3 result: f0: 0 0 0 0 f1: 1 0 0 0 f2: 0 1 0 0 f3: 1 1 0 0 f4: 0 0 1 0 f5: 1 0 1 0 f6: 0 1 1 0 f7: 1 1 1 0 f8: 0 0 0 1 f9: 1 0 0 1 f10: 0 1 0 1 f11: 1 1 0 1 f12: 0 0 1 1 f13: 1 0 1 1 f14: 0 1 1 1 f15: 1 1 1 1

The point is that even if a function is defined by a completely different algorithm (and thus lexically different), it can be reduced to a table lookup, where the size of the table is defined by the number of bits in the input. For instance from the functions above, isOdd() is the same as f10() and isPrime() is the same as f12().

Now, if we take any function above, we can find another function in the table that provides correct answers for 1 - Fn(i). For instance for f12() we have results 0 0 1 1, so we need a function that provides results 1 1 0 0. This is f3(). This is clearly a function that is already in the set.

If there are more bits than 2 available for i, the amount of different functions just grows, but is still limited in the same way as with a 2-bit input. So in order for the proof to work, input variables need to have infinite number of bits.

petermcneeley• 8 years ago

Yes it is actually the infinite that is at the core of all these problems. Same with the incomputability of https://en.wikipedia.org/wiki/Kolmogorov_complexity . If you simply think in terms of bits (the finite) none of these problems exist as one can simply search all permutations.

smadge• 8 years ago

First, there are many language who’s default integer type are not fixed bit width. For example Haskell and Python can represent arbitrarily large integers out of the box, limited only by available memory. Second, it is not too difficult to implement these “big integers” in any language. For example, I think java has something called a BigInteger class. Arguably if your “integer” type has fixed but width, it’s categorically not an integer. Third, two of the major underlying theoretical models of computation, Turing machines and Churche’s lambda calculus, allow arbitrary “memory” sizes and arbitrarily large integers. For example the universal Turing machine is imagined as operating over an infinitely long ticker tape. The objection you raise is a theoretical nonissue and I give the author some leeway to make this concept more accessible.

invincing2• 8 years ago

I think it's important to know when a theoretical framework can be applied to the full extent and when the real-life situation is actually a subset that behaves differently.

In this case the problem is solvable within the subset presented by the JavaScript language, but there are other cases where applying theory directly to real life constructs without considering the differences can lead to buggy code. For instance floating point numbers come to mind immediately.

I agree that discussions like this are sidetracking the whole point of a good article, but in order to avoid that, I'd use pseudo-code instead of a real language for presenting concepts like this.

Gödel’s First Incompleteness Theorem for Programmers

Related Stories