8 ms·

Gödel’s First Incompleteness Theorem for Programmers

63 points by dvt 9y ago

perfmode 9y ago
I love proofs of impossibility. Thanks for sharing
- dvt 9y ago
  Thanks, I enjoyed writing it!
cousin_it 9y 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 https://www.scottaaronson.com/blog/?p=710
OtterCoder 9y 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 9y ago
  Not inexpressible. Unprovable. There could be a set of correct programs that could never be proven correct by a type checker, for example.
- dvt 9y 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.
davrosthedalek 9y 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?
- dvt 9y 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.
  - davrosthedalek 9y 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?
rrauenza 9y 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 9y 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.
- dvt 9y 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 9y 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.
- dvt 9y ago
  Thanks! Glad you enjoyed it.
invincing 9y 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 9y 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 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 9y ago

63 points by dvt 9y ago

perfmode 9y ago

I love proofs of impossibility. Thanks for sharing

dvt 9y ago
Thanks, I enjoyed writing it!

cousin_it 9y 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 https://www.scottaaronson.com/blog/?p=710

OtterCoder 9y 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 9y ago
Not inexpressible. Unprovable. There could be a set of correct programs that could never be proven correct by a type checker, for example.
dvt 9y 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.

davrosthedalek 9y 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?

dvt 9y 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.
- davrosthedalek 9y 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?

rrauenza 9y 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 9y 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.
dvt 9y 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 9y 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.

dvt 9y ago
Thanks! Glad you enjoyed it.

invincing 9y 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 9y 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 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 9y ago