Re:Homotopy Type Theory (2012) [pdf]
by pgustafs on Tuesday October 27, 2020 @11:24PM
(#24914783)
Thanks for the interesting discussion. My main point of disagreement re:foundations is that in my view a central criterion for a foundational system is easy translation of common mathematical discourse into formal proofs. Otherwise, it seems that the coherence of ordinary mathematical discourse must be an article of faith.
[ Parent
| on HN ]
I don't have time to explain in detail at the moment, but I recommend reading about the history of set theory and the problems that the introduction of ZFC was meant to solve. I think you'll agree that they were both important and have nothing to do with proof verification.
More generally, it's not clear to me why you necessarily want the language you use to rigorously investigate the foundations of mathematics to be the same one you use to do proof verification. ZFC – and set-theoretic approaches more broadly – facilitate proving things about mathematics (meta-mathematical theorems), and for that they are very useful. E.g., the strength of a theory is equivalent to the size of the cardinals it assumes, loosely speaking [1].