> Similarly, if we could prove the axiom of choice from the ZF axioms, we would have to either accept it as true, or completely rework all the foundations of math.
And the footnote following this statement:
> At the beginning of the 20th century, Bertrand Russell and others found deep contradictions in the naive version of set theory in use at the time, and the ZF axioms were developed to avoid those problems. But we’d rather avoid doing it again.
My understanding is that the “constructive” mathematicians objected strenuously to these proposed foundational “solutions”. It’s starting to look like they may have been on to something, as there is an ongoing effort (since 2013 at least) to recast the foundations in a manner that accommodates both traditional and intuitionistic approaches.
Short anecdote to confirm that this might gain traction: I’m a comp sci PhD student (focus on cryptography) and just yesterday I met with a math professor to ask her to serve on my advising committee. I had some brief run-ins with Homotopy Type Theory (the proposed “new foundations”) and was hoping she might be familiar with it—as it turns out, some of her own students had recently convinced her to start a weekly jam session where they gradually work through the HoTT textbook. She invited me to join them and I eagerly accepted :-)
And the footnote following this statement:
> At the beginning of the 20th century, Bertrand Russell and others found deep contradictions in the naive version of set theory in use at the time, and the ZF axioms were developed to avoid those problems. But we’d rather avoid doing it again.
My understanding is that the “constructive” mathematicians objected strenuously to these proposed foundational “solutions”. It’s starting to look like they may have been on to something, as there is an ongoing effort (since 2013 at least) to recast the foundations in a manner that accommodates both traditional and intuitionistic approaches.
Short anecdote to confirm that this might gain traction: I’m a comp sci PhD student (focus on cryptography) and just yesterday I met with a math professor to ask her to serve on my advising committee. I had some brief run-ins with Homotopy Type Theory (the proposed “new foundations”) and was hoping she might be familiar with it—as it turns out, some of her own students had recently convinced her to start a weekly jam session where they gradually work through the HoTT textbook. She invited me to join them and I eagerly accepted :-)