4 ms·

I find it quite funny that, even as a research level scientist, he treats Gödel theorems like nice pop-science favourite novelty results. It didn't really close

I find it quite funny that, even as a research level scientist, he treats Gödel theorems like nice pop-science favourite novelty results. It didn't really close any mathematical domain of inquiry, on the contrary it opened new research areas in proof theory and set theory that are very much active, thanks to computers. These were debates within the Bourbaki group between first-order theories and second-order theories (where you can quantify over formulas), since the latter is complete; but the first one can be investigated much more deeply and leads to a rich variety of results. You can build many theories, more or less arbitrary, to refine your intuition. Gödel's result make it harder to have objective mathematical standards to show why one is better than the other, the standards have to be external. Beyond that, Gödel wanted to arrive to an alternate set theory that had a definite answer to the continuum hypothesis, because consistency and provability are not really goals in themselves, but simply prerequisites.

throwaway81523 4y ago
> It didn't really close any mathematical domain of inquiry, It supposedly killed off the Hilbert program, which sought a consistency and completeness proof for mathematics, and a mechanized procedure for deciding arbitrary mathematical propositions.
- woolion 4y ago
  Well yes, that's my point. Hilbert's program would have killed a lot of research domains. Its success would have meant we found the perfect set of axioms, supposedly ZFC, and that for each theorem you could easily check its proof via a program. An "end of history" for mathematics. Since it's not the case now we have HoTT and other approaches to fill in the gaps, or see things through different perspectives.
  - andrepd 4y ago
    Well you do have automatic proof-checking procedures, they are just not decision procedures (because the theory is not complete).
    - woolion 4y ago
      Right. But this is only a proof in a given theory. If ZFC was consistent and complete, it would have had complete dominance over the notion of truth, even if it had some quirks (as the joke goes, "The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn’s lemma?"). It is not the case, so there are competing theories with different consequences, and the world is more interesting because of that. What I'm trying to get at is that mathematical truth people care about goes beyond provability, and that is the case in good part because of incompleteness.
  - mannerheim 4y ago
    Not necessarily. There are decidable theories for which there exist algorithms that can prove or disprove any statement, but run in super-exponential time.

throwaway81523 4y ago

> It didn't really close any mathematical domain of inquiry, It supposedly killed off the Hilbert program, which sought a consistency and completeness proof for mathematics, and a mechanized procedure for deciding arbitrary mathematical propositions.

woolion 4y ago
Well yes, that's my point. Hilbert's program would have killed a lot of research domains. Its success would have meant we found the perfect set of axioms, supposedly ZFC, and that for each theorem you could easily check its proof via a program. An "end of history" for mathematics. Since it's not the case now we have HoTT and other approaches to fill in the gaps, or see things through different perspectives.
- andrepd 4y ago
  Well you do have automatic proof-checking procedures, they are just not decision procedures (because the theory is not complete).
  - woolion 4y ago
    Right. But this is only a proof in a given theory. If ZFC was consistent and complete, it would have had complete dominance over the notion of truth, even if it had some quirks (as the joke goes, "The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn’s lemma?"). It is not the case, so there are competing theories with different consequences, and the world is more interesting because of that. What I'm trying to get at is that mathematical truth people care about goes beyond provability, and that is the case in good part because of incompleteness.
- mannerheim 4y ago
  Not necessarily. There are decidable theories for which there exist algorithms that can prove or disprove any statement, but run in super-exponential time.