37 ms·
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, suppo
by 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 agoWell you do have automatic proof-checking procedures, they are just not decision procedures (because the theory is not complete).
- woolion 4y agoRight. 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 agoNot necessarily. There are decidable theories for which there exist algorithms that can prove or disprove any statement, but run in super-exponential time.