6 ms·

The complete story of Gödel incompleteness

81 points by herodotus 3y ago

082349872349872 3y ago
> If we allow experimental evidence That's a remarkably big if. (Consider the history of the parallel postulate: https://en.wikipedia.org/wiki/Parallel_postulate#History https://en.wikipedia.org/wiki/Parallel_postulate#History )
- nyrikki 3y ago
  > With a little more effort we can establish the same for any enumerable set of axioms. This is a case of presentism, which due to the work of Gödel we accept the costs of the implications of his findings. RE is semi-decidable, meaning we can find yes-instances, although some yes-instances may be false. RE+co-RE=R, when the author is only referencing RE. Failure as negation does have its place but it also is what will probably block strong-AI. Also note that presburger arithmetic, FoL with (+,=) or (*,=) is fully decidable. But proofs require double exponential time. Superfactorial time isn't practical. Same with attention in feed forward networks requiring exponential time with a reduction in expressability. This is a lower bound for negation through exhaustion in zero order logic through the strong exponential time theorem. The loss of reliable negation: (¬) in all but the weakest logic forms in the general case has huge practical implications for all but the most trivial problems. Unless you are lucky enough to have a fully decidable model aka recursive, the costs are high. PA was shown to be consistent with transfinite induction BTW. But that is because the natural numbers are well ordered. But transformers with soft attention being limited to solving problems in TC^0 with failure as negation is a very real cost of Gödels (in) completeness theorems.
  - yodsanklai 3y ago
    How relevant are these considerations for practical use cases? Specifically, for all practical purpose, it is sufficient to have probabilistic guarantees. Suppose an AI is able to generate mathematical proofs as well as humans, it wouldn't really matter if in theory "they are limited to solving problems in TC^0 with failure as negation"
    - nyrikki 3y ago
      While TC^0 can divide or multiply through say FFT, it actually can't do counters or addition which I am pretty sure requires TC^1 or Log-depth Threshold Circuits. LTSM is much more powerful.
  - readyplayernull 3y ago
    > Failure as negation does have its place but it also is what will probably block strong-AI. Interesting, could you please explain more on this?
    - nyrikki 3y ago
      The deduction principle turns out to be invalid for weak rejections and strong AI requires it. Consider strong negation: Did Homer write the Iliad? No, he did not. VS a too computationally expensive system with true,false,other with no knowledge of Homer: Did Homer write the Iliad? No, Homer did not exist. Vs negation as failure of binary threshold ANNs: Did Homer write the Iliad? No. Transformers explicitly can find known unknowns, unknowable unknowns (eg future unknowns), etc.. But exhaustive unknowns may or may not be valid. There is a lot more to it, but strong AI requires universal quantification, ML is existential quantification. The above is just one way to think about why Word sense disambiguation and ATP are though to be AI-complete.
  - drdeca 3y ago
    > Same with attention in feed forward networks requiring exponential time with a reduction in expressability. Huh? Can you say more about that? What takes exponential time with transformers?
    - nyrikki 3y ago
      > We prove that the time complexity of self-attention is necessarily quadratic in the input length, unless the Strong Exponential Time Hypothesis (SETH) is false. This argument holds even if the attention computation is performed only approximately, and for a variety of attention mechanisms. https://proceedings.mlr.press/v201/duman-keles23a/duman-keles23a.pdf https://proceedings.mlr.press/v201/duman-keles23a/duman-kele...
      - drdeca 3y ago
        Thanks! But, quadratic time complexity (which I had heard that attention requires, which doesn't surprise me) is not exponential time. I acknowledge that they related this to the assumption of the SETH (which surprises me a little). But, this doesn't mean that transformers take exponential time. I don't think I understood what you meant by the "with a reduction in expressability" part of the statement, so maybe that is the reason behind me not following.
- daxfohl 3y ago
  Though note that was a question of possible redundancy, not possible inconsistency. Still, the outcome is probably roughly the same. We'd replace the inconsistent axiom with something similar and 99.99% of existing practical math would still follow, and only a few intentionally specious constructions would fail. (It kind of begs the question of whether math follows from the axioms we want or axioms follow from the math we want). Plus perhaps some new math would start to unfold as we begin to explore the inconsistent axiom's subtleties.
  - Radim 3y ago
    > (It kind of begs the question of whether math follows from the axioms we want or axioms follow from the math we want). Plus perhaps some new math would start to unfold as we begin to explore the inconsistent axiom's subtleties. Only tangentially related, but the same idea comes to mind reading Terence Tao's masterpiece on "Smoothed asymptotics" for divergent infinite sums (e.g. the infamous 1+2+3+4+… = -1/12): https://terrytao.wordpress.com/2010/04/10/the-euler-maclaurin-formula-bernoulli-numbers-the-zeta-function-and-real-variable-analytic-continuation/ https://terrytao.wordpress.com/2010/04/10/the-euler-maclauri... Our intuitive interpretation (Σn must be infinite! and surely positive! never -1/12) fails miserably for such infinite series, in the sense that "practical experiments" (QM) hint at reality preferring that bizarro -1/12 interpretation instead. Who is at fault here – our seemingly iron-clad intuition or the experiments? And why the disconnect? Like you say, what new math unfolds once we accept and internalize this new interpretation and adjust our intuition? Tao's piece offers an excellent basis for that. While we may come up with any interpretations and axioms we like, experiment is the final arbiter on which of these "math worlds" are real.
deleted 3y ago
[deleted]
hackandthink 3y ago
"Before this, logic had been strictly syntactical and proof theoretic" Frege disagrees: "Just as the concept point belongs to geometry, so logic, too, has its own concepts and relations; and it is only in virtue of this that it can have a content. Toward what is thus proper to it, its relation is not at all formal." https://plato.stanford.edu/entries/frege/#FreConLog https://plato.stanford.edu/entries/frege/#FreConLog
- pulisse 3y ago
  TFA uses sloppy phrasing, but it's correct. The claim is not that earlier logicians such as Frege viewed logical concepts as meaningless. It's that, before Tarski and Gödel, no one clearly distinguished syntax and semantics, and so earlier logicians lacked the conceptual resources to describe the difference between truth and provability, let alone investigate their relationship. (Frege only ever considers a single semantics for any formal system.)
  - hackandthink 3y ago
    "It's that, before Tarski and Gödel, no one clearly distinguished syntax and semantics" I think this is right, but Hilbert came already close much earlier. But "Before this, logic had been strictly syntactical and proof theoretic" is at least misleading. Traditional logic was more conceptional. Frege's "formalism" was a great innovation, but he remained within the conceptual tradition (Frege-Hilbert controversy). "What Hilbert offers us, in 1899, is a systematic and powerful technique that can be used across all formalized disciplines to do just this: to prove consistency and independence. In doing so, he lays the groundwork, in concert with various of his contemporaries, for the emergence of contemporary model-theoretic techniques." https://plato.stanford.edu/entries/frege-hilbert/ https://plato.stanford.edu/entries/frege-hilbert/
jekude 3y ago
Would anyone happen to have a recommendation for someone hoping to make Gödel's incompleteness theorem "click"? It feels like every time I reapproach it, I have to start the intuition building all over again.
- Areading314 3y ago
  Read gödel, escher, bach by Douglas Hofstaedter
  - mayd 3y ago
    As the late Martin Gardiner opined: "Every few decades an unknown author brings out a book of such depth, clarity, range, wit, beauty and originality that it is recognised at once as a major literary event. This is such a work." Nevertheless, Infinity and the Mind: The Science and Philosophy of the Infinite by Rudy Rucker is, in my opinion, a better choice for the mathematically inclined layman interested in Goedel's discoveries and plenty of related mathematics. Rucker's book even includes an account of his (somewhat over-enfusive) meeting with the great man.
- bsdpufferfish 3y ago
  Why are you interested? I recommend the short book "Godel's proof". Godel's work is wrapped up in historical context which is both interesting and distracting from the core idea. For example, Bertrand's Russells' work and book isn't really essential, it's just the system which Godel worked in to do his proof.
- steppi 3y ago
  There’s a wonderful book on the subject by Raymond Smullyan, of knights and knaves recreational math puzzle fame which helped make it click for me. https://lib.undercaffeinated.xyz/get/pdf/5823 https://lib.undercaffeinated.xyz/get/pdf/5823
  - johnthescott 3y ago
    K&K i would recommend as a first read on logic. i found GEB to be a bit long winded.
bionhoward 3y ago
I just can't get this dumb question out of my head: How could any "incompleteness theorem" ever be completely true?
- gjm11 3y ago
  In the same way as a theorem that says "the sequence of prime numbers is infinite" can be finitely long, or a theorem that says "the square root of 2 is irrational" can be rational :-). If the theorem just said "everything is incomplete", maybe that would be a problem, but that isn't what it says. Goedel's (first) incompleteness theorem says: if you have a formal system with such-and-such properties, then there have to be statements it can neither prove nor disprove. The theorem itself isn't a formal system with such-and-such properties. It isn't talking about itself. (Amusing though it would be if it were, since one of the neat things about Goedel's proof is the way it gets mathematical statements to kinda-sorta talk about themselves.)
- dandanua 3y ago
  The correct way to understand it is this: "We can't pack (i.e. compress) all the mathematical knowledge in a finite set of axioms and rules." This statement doesn't look paradoxical.
VirusNewbie 3y ago
I can prove a subset of peano arithmetic is complete and consistent though. And that’s usually enough.
- jpt4 3y ago
  Not using that same subset, however (unless working with a Self-Verifying Theory [0]). [0] https://en.wikipedia.org/wiki/Self-verifying_theories https://en.wikipedia.org/wiki/Self-verifying_theories

81 points by herodotus 3y ago

> If we allow experimental evidence That's a remarkably big if. (Consider the history of the parallel postulate: https://en.wikipedia.org/wiki/Parallel_postulate#History https://en.wikipedia.org/wiki/Parallel_postulate#History )

nyrikki 3y ago
> With a little more effort we can establish the same for any enumerable set of axioms. This is a case of presentism, which due to the work of Gödel we accept the costs of the implications of his findings. RE is semi-decidable, meaning we can find yes-instances, although some yes-instances may be false. RE+co-RE=R, when the author is only referencing RE. Failure as negation does have its place but it also is what will probably block strong-AI. Also note that presburger arithmetic, FoL with (+,=) or (*,=) is fully decidable. But proofs require double exponential time. Superfactorial time isn't practical. Same with attention in feed forward networks requiring exponential time with a reduction in expressability. This is a lower bound for negation through exhaustion in zero order logic through the strong exponential time theorem. The loss of reliable negation: (¬) in all but the weakest logic forms in the general case has huge practical implications for all but the most trivial problems. Unless you are lucky enough to have a fully decidable model aka recursive, the costs are high. PA was shown to be consistent with transfinite induction BTW. But that is because the natural numbers are well ordered. But transformers with soft attention being limited to solving problems in TC^0 with failure as negation is a very real cost of Gödels (in) completeness theorems.
- yodsanklai 3y ago
  How relevant are these considerations for practical use cases? Specifically, for all practical purpose, it is sufficient to have probabilistic guarantees. Suppose an AI is able to generate mathematical proofs as well as humans, it wouldn't really matter if in theory "they are limited to solving problems in TC^0 with failure as negation"
  - nyrikki 3y ago
    While TC^0 can divide or multiply through say FFT, it actually can't do counters or addition which I am pretty sure requires TC^1 or Log-depth Threshold Circuits. LTSM is much more powerful.
- readyplayernull 3y ago
  > Failure as negation does have its place but it also is what will probably block strong-AI. Interesting, could you please explain more on this?
  - nyrikki 3y ago
    The deduction principle turns out to be invalid for weak rejections and strong AI requires it. Consider strong negation: Did Homer write the Iliad? No, he did not. VS a too computationally expensive system with true,false,other with no knowledge of Homer: Did Homer write the Iliad? No, Homer did not exist. Vs negation as failure of binary threshold ANNs: Did Homer write the Iliad? No. Transformers explicitly can find known unknowns, unknowable unknowns (eg future unknowns), etc.. But exhaustive unknowns may or may not be valid. There is a lot more to it, but strong AI requires universal quantification, ML is existential quantification. The above is just one way to think about why Word sense disambiguation and ATP are though to be AI-complete.
- drdeca 3y ago
  > Same with attention in feed forward networks requiring exponential time with a reduction in expressability. Huh? Can you say more about that? What takes exponential time with transformers?
  - nyrikki 3y ago
    > We prove that the time complexity of self-attention is necessarily quadratic in the input length, unless the Strong Exponential Time Hypothesis (SETH) is false. This argument holds even if the attention computation is performed only approximately, and for a variety of attention mechanisms. https://proceedings.mlr.press/v201/duman-keles23a/duman-keles23a.pdf https://proceedings.mlr.press/v201/duman-keles23a/duman-kele...
    - drdeca 3y ago
      Thanks! But, quadratic time complexity (which I had heard that attention requires, which doesn't surprise me) is not exponential time. I acknowledge that they related this to the assumption of the SETH (which surprises me a little). But, this doesn't mean that transformers take exponential time. I don't think I understood what you meant by the "with a reduction in expressability" part of the statement, so maybe that is the reason behind me not following.
daxfohl 3y ago
Though note that was a question of possible redundancy, not possible inconsistency. Still, the outcome is probably roughly the same. We'd replace the inconsistent axiom with something similar and 99.99% of existing practical math would still follow, and only a few intentionally specious constructions would fail. (It kind of begs the question of whether math follows from the axioms we want or axioms follow from the math we want). Plus perhaps some new math would start to unfold as we begin to explore the inconsistent axiom's subtleties.
- Radim 3y ago
  > (It kind of begs the question of whether math follows from the axioms we want or axioms follow from the math we want). Plus perhaps some new math would start to unfold as we begin to explore the inconsistent axiom's subtleties. Only tangentially related, but the same idea comes to mind reading Terence Tao's masterpiece on "Smoothed asymptotics" for divergent infinite sums (e.g. the infamous 1+2+3+4+… = -1/12): https://terrytao.wordpress.com/2010/04/10/the-euler-maclaurin-formula-bernoulli-numbers-the-zeta-function-and-real-variable-analytic-continuation/ https://terrytao.wordpress.com/2010/04/10/the-euler-maclauri... Our intuitive interpretation (Σn must be infinite! and surely positive! never -1/12) fails miserably for such infinite series, in the sense that "practical experiments" (QM) hint at reality preferring that bizarro -1/12 interpretation instead. Who is at fault here – our seemingly iron-clad intuition or the experiments? And why the disconnect? Like you say, what new math unfolds once we accept and internalize this new interpretation and adjust our intuition? Tao's piece offers an excellent basis for that. While we may come up with any interpretations and axioms we like, experiment is the final arbiter on which of these "math worlds" are real.

deleted 3y ago

[deleted]

hackandthink 3y ago

"Before this, logic had been strictly syntactical and proof theoretic" Frege disagrees: "Just as the concept point belongs to geometry, so logic, too, has its own concepts and relations; and it is only in virtue of this that it can have a content. Toward what is thus proper to it, its relation is not at all formal." https://plato.stanford.edu/entries/frege/#FreConLog https://plato.stanford.edu/entries/frege/#FreConLog

pulisse 3y ago
TFA uses sloppy phrasing, but it's correct. The claim is not that earlier logicians such as Frege viewed logical concepts as meaningless. It's that, before Tarski and Gödel, no one clearly distinguished syntax and semantics, and so earlier logicians lacked the conceptual resources to describe the difference between truth and provability, let alone investigate their relationship. (Frege only ever considers a single semantics for any formal system.)
- hackandthink 3y ago
  "It's that, before Tarski and Gödel, no one clearly distinguished syntax and semantics" I think this is right, but Hilbert came already close much earlier. But "Before this, logic had been strictly syntactical and proof theoretic" is at least misleading. Traditional logic was more conceptional. Frege's "formalism" was a great innovation, but he remained within the conceptual tradition (Frege-Hilbert controversy). "What Hilbert offers us, in 1899, is a systematic and powerful technique that can be used across all formalized disciplines to do just this: to prove consistency and independence. In doing so, he lays the groundwork, in concert with various of his contemporaries, for the emergence of contemporary model-theoretic techniques." https://plato.stanford.edu/entries/frege-hilbert/ https://plato.stanford.edu/entries/frege-hilbert/

jekude 3y ago

Would anyone happen to have a recommendation for someone hoping to make Gödel's incompleteness theorem "click"? It feels like every time I reapproach it, I have to start the intuition building all over again.

Areading314 3y ago
Read gödel, escher, bach by Douglas Hofstaedter
- mayd 3y ago
  As the late Martin Gardiner opined: "Every few decades an unknown author brings out a book of such depth, clarity, range, wit, beauty and originality that it is recognised at once as a major literary event. This is such a work." Nevertheless, Infinity and the Mind: The Science and Philosophy of the Infinite by Rudy Rucker is, in my opinion, a better choice for the mathematically inclined layman interested in Goedel's discoveries and plenty of related mathematics. Rucker's book even includes an account of his (somewhat over-enfusive) meeting with the great man.
bsdpufferfish 3y ago
Why are you interested? I recommend the short book "Godel's proof". Godel's work is wrapped up in historical context which is both interesting and distracting from the core idea. For example, Bertrand's Russells' work and book isn't really essential, it's just the system which Godel worked in to do his proof.
steppi 3y ago
There’s a wonderful book on the subject by Raymond Smullyan, of knights and knaves recreational math puzzle fame which helped make it click for me. https://lib.undercaffeinated.xyz/get/pdf/5823 https://lib.undercaffeinated.xyz/get/pdf/5823
- johnthescott 3y ago
  K&K i would recommend as a first read on logic. i found GEB to be a bit long winded.

bionhoward 3y ago

I just can't get this dumb question out of my head: How could any "incompleteness theorem" ever be completely true?

gjm11 3y ago
In the same way as a theorem that says "the sequence of prime numbers is infinite" can be finitely long, or a theorem that says "the square root of 2 is irrational" can be rational :-). If the theorem just said "everything is incomplete", maybe that would be a problem, but that isn't what it says. Goedel's (first) incompleteness theorem says: if you have a formal system with such-and-such properties, then there have to be statements it can neither prove nor disprove. The theorem itself isn't a formal system with such-and-such properties. It isn't talking about itself. (Amusing though it would be if it were, since one of the neat things about Goedel's proof is the way it gets mathematical statements to kinda-sorta talk about themselves.)
dandanua 3y ago
The correct way to understand it is this: "We can't pack (i.e. compress) all the mathematical knowledge in a finite set of axioms and rules." This statement doesn't look paradoxical.

VirusNewbie 3y ago

I can prove a subset of peano arithmetic is complete and consistent though. And that’s usually enough.

jpt4 3y ago
Not using that same subset, however (unless working with a Self-Verifying Theory [0]). [0] https://en.wikipedia.org/wiki/Self-verifying_theories https://en.wikipedia.org/wiki/Self-verifying_theories