6 ms·

are there any practical impacts (direct or indirect) of these results?

archi42 7y ago
You want to ask Hilbert ;-) Yes, there are. You/we can not programmatically derive all mathematical truths from ZFC ("the basic math axioms"). E.g. we recently had the Collatz Conjecture here on HN [1], and I strongly suspect that it can be neither proven nor falsified. Also, if one could solve the Halting Problem that would be quite useful. Thanks to Gödel we know that we might be not just stupid apes, but that some things are indeed undecidable (even if they must be true or false). [1] https://news.ycombinator.com/item?id=21780068 https://news.ycombinator.com/item?id=21780068
- zozbot234 7y ago
  Specifically, "mathematical truths" here meams statements that, while logically independent from ZFC, are not independent from e.g. ZFC plus Con(ZFC). Or Con(Con(ZFC)), or Con(for any n, Con^n(ZFC)), or even more elaborate varieties. AIUI, part of what Recursion theory does is characterize these "true" consistency statements. The field is closely related to, e.g. halting oracles in TCS.
  - ProfHewitt 7y ago
    True propositions of sets are those that hold in the up to unique isomorphism model of the theory Ordinals defined here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802
- Yajirobe 7y ago
  > some things are indeed undecidable (even if they must be true or false). What does it mean 'even if they must be true or false'? What does truth and falsehood mean if you cannot in theory prove/disprove a proposition? You are suggesting the existence of some sort of Platonic realm, where propositions have definite truth/falsehood values, while at the same time being inaccessible to us.
  - lou1306 7y ago
    The propositions themselves are not inaccessible, but there is no way to automate the process of testing their truthiness in a way that always works. That is the usual menaning of undecidability.
    - Yajirobe 7y ago
      > The propositions themselves are not inaccessible Yes, I know. I meant that their truth value is inaccessible. What I'm saying is that claiming 'some things are indeed undecidable (even if they must be true or false)' suggests the existence of a Platonic realm with an existing truth value. If a proposition is undecidable, it makes no sense to talk about whether 'it actually is true/false', because truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition.
      - zozbot234 7y ago
        > truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition. The thing is, this isn't necessarily the case. "Proving/disproving" a proposition can only be done starting from a set of axioms that are independently thought of as "true". But if you think of, e.g. ZFC as true, you'll also think of Con(ZFC) as true, even though the statement of Con(ZFC) can't be proven from ZFC. Similarly for Con(Con(ZFC)) and many sorts of increasingly-complex "consistency" statements.
      - Scarblac 7y ago
        The law of the excluded middle says that for all propositions, either it or its negation must be true. But Godel showed that there exist propositions for which neither can be proven.
        ProfHewitt 7y ago
        The Law of Excluded Middle says: ⊢(Ψ or ~Ψ) In inferential incompleteness says that there is a proposition Ψ such that: (⊬Ψ) and (⊬~Ψ)
zozbot234 7y ago
Not really. Gödel's theorem only proved that the specific kind of "mechanization of mathematics" that's implied by Hilbert's program as originally devised is impossible. The wiki has a nice section on varieties of Hilbert's program after Gödel https://en.wikipedia.org/wiki/Hilbert%27s_program#Hilbert%27s_program_after_G%C3%B6del https://en.wikipedia.org/wiki/Hilbert%27s_program#Hilbert%27... , citing (Zach, 2006) https://arxiv.org/abs/math/0508572 https://arxiv.org/abs/math/0508572 Of course from a slightly different POV there are plenty of practical implications, since e.g. unsolvability of the Halting problem can be viewed as a close variant of Gödel's results.
mikorym 7y ago
Yes. Because of Gödel, von Neumann and others stopped trying to build machines that can prove anything. Of course, following the critiques and further revisions of Zermelo’s set theory by Fraenkel, Skolem, Hilbert and von Neumann, a young mathematician by the name of Kurt Gödel in 1930 published a paper which would effectively end von Neumann’s efforts in formalist set theory, and indeed Hilbert’s formalist program altogether, his theorem of incompleteness. von Neumann happened to be in the audience when Gödel first presented it [1] [1] https://medium.com/cantors-paradise/the-unparalleled-genius-of-john-von-neumann-791bb9f42a2d https://medium.com/cantors-paradise/the-unparalleled-genius-...
mar77i 7y ago
For one practical example, Gödel's incompleteness is directly related to decidability problems in CS. there's this glorious liar paradox machine discussed by Computerphile [0]. [0] https://www.youtube.com/watch?v=macM_MtS_w4 https://www.youtube.com/watch?v=macM_MtS_w4
chewxy 7y ago
There is one - a particular viewpoint on the Incompleteness Theorems imply that you cannot in general tell if a program encoded on a UTM will halt or not.
yters 7y ago
The computer theory version of Godel's result is the halting problem, and that is applicable all over the place, in the same way that physical conservation laws imply a large variety of invention are impossible. For example, it is impossible in general to understand what an English sentence says, because that sentence may describe the operation of an arbitrary program, and understanding an arbitrary program is undecidable. Another example, it is impossible to detect all variants of malicious programs, because that requires understanding what all programs do, which requires identifying whether an arbitrary program halts or not. Yet another example, optimal machine learning is impossible, since that is based on Solomonoff induction, based on Kolmogorov complexity, which is uncomputable due to the halting problem. And another off the top of my head, it is impossible to create a general program creating program, such that you give it a well defined specification and it spits out a program that meets the requirements, if the requirements are satisfiable, since that requires solving the halting problem. Finally, humans, while not optimally satisfying all the above tasks, do quite a decent job at these tasks, which is surprising if humans themselves were some sort of algorithm. So, this strongly suggests the human mind is doing some operation beyond computation, which in turn would imply that human intelligence level AI is impossible in theory, and thus impossible in practice. Furthermore, if the human mind is indeed doing something uncomputable, this has technological implications that human in the loop computation approaches are inherently more powerful than computation alone, a vastly under researched concept, although arguably the secret to the success of most AI/ML/datamining companies these days, such as Google, Facebook, Amazon, and Palantir. And the software industry in general is proof of this concept that humans are program generating processes performing much better than the halting problem would lead one to expect if humans were indeed mere computation. Anyways, a whole bunch of impossibility implications, which have the practical application of protecting your wallet from comp. sci. snake oil salesmen, and the intriguing possibility 'beyond computation' technology.
- pure-awesome 7y ago
  > Finally, humans, while not optimally satisfying all the above tasks, do quite a decent job at these tasks, which is surprising if humans themselves were some sort of algorithm. Whilst I agree with everything in your comment before this point, I don't agree with this. There is a very big difference between almost achieving something and actually achieving it. For example, there exist algorithms which are able to determine whether a given program halts, for a large class of programs, or to give some probability that a program halts prior to some point, even if they are unable to solve the general halting problem. So you haven't really argued that humans are doing something computers can't do. In addition, I take issue with your statement that humans "do quite a decent job at these tasks". On the face of it, I agree that yes, (when sufficiently motivated) (some) humans do indeed do a pretty good job of e.g. proving mathematical theorems and writing programs that halt when they should. Certainly better than the best computers we can build. But that "pretty good" is a _far_ cry from the optimality referenced in the theorems you've stated. And if you are using this "pretty good" to indicate that humans are better than any possible algorithm, that argument doesn't follow-through. I think that human-level algorithms are in principle possible. They will have to incorporate a lot of probability and approximate results and the like, and likely will have something similar to "intuition" where the path from input to output is not clear, whether to human onlookers or to the algorithm itself (whatever that might mean). We already see hints of this today with our deep learning algorithms. Not to say that we are necessarily close to achieving this, or that we ever will, but on the other hand it might very well be just around the corner!

You want to ask Hilbert ;-) Yes, there are. You/we can not programmatically derive all mathematical truths from ZFC ("the basic math axioms"). E.g. we recently had the Collatz Conjecture here on HN [1], and I strongly suspect that it can be neither proven nor falsified. Also, if one could solve the Halting Problem that would be quite useful. Thanks to Gödel we know that we might be not just stupid apes, but that some things are indeed undecidable (even if they must be true or false). [1] https://news.ycombinator.com/item?id=21780068 https://news.ycombinator.com/item?id=21780068

zozbot234 7y ago
Specifically, "mathematical truths" here meams statements that, while logically independent from ZFC, are not independent from e.g. ZFC plus Con(ZFC). Or Con(Con(ZFC)), or Con(for any n, Con^n(ZFC)), or even more elaborate varieties. AIUI, part of what Recursion theory does is characterize these "true" consistency statements. The field is closely related to, e.g. halting oracles in TCS.
- ProfHewitt 7y ago
  True propositions of sets are those that hold in the up to unique isomorphism model of the theory Ordinals defined here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802
Yajirobe 7y ago
> some things are indeed undecidable (even if they must be true or false). What does it mean 'even if they must be true or false'? What does truth and falsehood mean if you cannot in theory prove/disprove a proposition? You are suggesting the existence of some sort of Platonic realm, where propositions have definite truth/falsehood values, while at the same time being inaccessible to us.
- lou1306 7y ago
  The propositions themselves are not inaccessible, but there is no way to automate the process of testing their truthiness in a way that always works. That is the usual menaning of undecidability.
  - Yajirobe 7y ago
    > The propositions themselves are not inaccessible Yes, I know. I meant that their truth value is inaccessible. What I'm saying is that claiming 'some things are indeed undecidable (even if they must be true or false)' suggests the existence of a Platonic realm with an existing truth value. If a proposition is undecidable, it makes no sense to talk about whether 'it actually is true/false', because truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition.
    - zozbot234 7y ago
      > truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition. The thing is, this isn't necessarily the case. "Proving/disproving" a proposition can only be done starting from a set of axioms that are independently thought of as "true". But if you think of, e.g. ZFC as true, you'll also think of Con(ZFC) as true, even though the statement of Con(ZFC) can't be proven from ZFC. Similarly for Con(Con(ZFC)) and many sorts of increasingly-complex "consistency" statements.
    - Scarblac 7y ago
      The law of the excluded middle says that for all propositions, either it or its negation must be true. But Godel showed that there exist propositions for which neither can be proven.
      - ProfHewitt 7y ago
        The Law of Excluded Middle says: ⊢(Ψ or ~Ψ) In inferential incompleteness says that there is a proposition Ψ such that: (⊬Ψ) and (⊬~Ψ)

zozbot234 7y ago

Not really. Gödel's theorem only proved that the specific kind of "mechanization of mathematics" that's implied by Hilbert's program as originally devised is impossible. The wiki has a nice section on varieties of Hilbert's program after Gödel https://en.wikipedia.org/wiki/Hilbert%27s_program#Hilbert%27s_program_after_G%C3%B6del https://en.wikipedia.org/wiki/Hilbert%27s_program#Hilbert%27... , citing (Zach, 2006) https://arxiv.org/abs/math/0508572 https://arxiv.org/abs/math/0508572 Of course from a slightly different POV there are plenty of practical implications, since e.g. unsolvability of the Halting problem can be viewed as a close variant of Gödel's results.

mikorym 7y ago

Yes. Because of Gödel, von Neumann and others stopped trying to build machines that can prove anything. Of course, following the critiques and further revisions of Zermelo’s set theory by Fraenkel, Skolem, Hilbert and von Neumann, a young mathematician by the name of Kurt Gödel in 1930 published a paper which would effectively end von Neumann’s efforts in formalist set theory, and indeed Hilbert’s formalist program altogether, his theorem of incompleteness. von Neumann happened to be in the audience when Gödel first presented it [1] [1] https://medium.com/cantors-paradise/the-unparalleled-genius-of-john-von-neumann-791bb9f42a2d https://medium.com/cantors-paradise/the-unparalleled-genius-...

mar77i 7y ago

For one practical example, Gödel's incompleteness is directly related to decidability problems in CS. there's this glorious liar paradox machine discussed by Computerphile [0]. [0] https://www.youtube.com/watch?v=macM_MtS_w4 https://www.youtube.com/watch?v=macM_MtS_w4

chewxy 7y ago

There is one - a particular viewpoint on the Incompleteness Theorems imply that you cannot in general tell if a program encoded on a UTM will halt or not.

yters 7y ago

The computer theory version of Godel's result is the halting problem, and that is applicable all over the place, in the same way that physical conservation laws imply a large variety of invention are impossible. For example, it is impossible in general to understand what an English sentence says, because that sentence may describe the operation of an arbitrary program, and understanding an arbitrary program is undecidable. Another example, it is impossible to detect all variants of malicious programs, because that requires understanding what all programs do, which requires identifying whether an arbitrary program halts or not. Yet another example, optimal machine learning is impossible, since that is based on Solomonoff induction, based on Kolmogorov complexity, which is uncomputable due to the halting problem. And another off the top of my head, it is impossible to create a general program creating program, such that you give it a well defined specification and it spits out a program that meets the requirements, if the requirements are satisfiable, since that requires solving the halting problem. Finally, humans, while not optimally satisfying all the above tasks, do quite a decent job at these tasks, which is surprising if humans themselves were some sort of algorithm. So, this strongly suggests the human mind is doing some operation beyond computation, which in turn would imply that human intelligence level AI is impossible in theory, and thus impossible in practice. Furthermore, if the human mind is indeed doing something uncomputable, this has technological implications that human in the loop computation approaches are inherently more powerful than computation alone, a vastly under researched concept, although arguably the secret to the success of most AI/ML/datamining companies these days, such as Google, Facebook, Amazon, and Palantir. And the software industry in general is proof of this concept that humans are program generating processes performing much better than the halting problem would lead one to expect if humans were indeed mere computation. Anyways, a whole bunch of impossibility implications, which have the practical application of protecting your wallet from comp. sci. snake oil salesmen, and the intriguing possibility 'beyond computation' technology.

pure-awesome 7y ago
> Finally, humans, while not optimally satisfying all the above tasks, do quite a decent job at these tasks, which is surprising if humans themselves were some sort of algorithm. Whilst I agree with everything in your comment before this point, I don't agree with this. There is a very big difference between almost achieving something and actually achieving it. For example, there exist algorithms which are able to determine whether a given program halts, for a large class of programs, or to give some probability that a program halts prior to some point, even if they are unable to solve the general halting problem. So you haven't really argued that humans are doing something computers can't do. In addition, I take issue with your statement that humans "do quite a decent job at these tasks". On the face of it, I agree that yes, (when sufficiently motivated) (some) humans do indeed do a pretty good job of e.g. proving mathematical theorems and writing programs that halt when they should. Certainly better than the best computers we can build. But that "pretty good" is a _far_ cry from the optimality referenced in the theorems you've stated. And if you are using this "pretty good" to indicate that humans are better than any possible algorithm, that argument doesn't follow-through. I think that human-level algorithms are in principle possible. They will have to incorporate a lot of probability and approximate results and the like, and likely will have something similar to "intuition" where the path from input to output is not clear, whether to human onlookers or to the algorithm itself (whatever that might mean). We already see hints of this today with our deep learning algorithms. Not to say that we are necessarily close to achieving this, or that we ever will, but on the other hand it might very well be just around the corner!