32 ms·

I don't think you should regard ZFC's purpose as proof verification. If you want verification, by all means use something else, as discussed in the link in my o

I don't think you should regard ZFC's purpose as proof verification. If you want verification, by all means use something else, as discussed in the link in my original post (which also addresses your scheme point – that's a problem common to most approaches so far!). If HoTT helps you prove theorems, great. In particular I could see it being of interest to people working in higher category theory (and such people have responded in other comments here!). My remarks were meant for the other 99% of mathematicians – most of whom go their entire lives without ever writing the word "category" in a paper.

pgustafs 6y ago
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.
- spekcular 6y ago
  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]. [1] https://en.wikipedia.org/wiki/Large_cardinal https://en.wikipedia.org/wiki/Large_cardinal
pgustafs 6y ago
We've hit the comment depth limit, so I'll reply here. > 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. Among other things, I want theorems about foundations to be useful to non-foundational mathematicians. Working on type theory can improve, at the very least, formal verification tools. In my view, traditional ZFC-based mathematical logic has a much smaller likelihood of being useful for regular mathematicians. For example, the vast majority of mathematicians will never explicitly assume the existence of a large cardinal in a paper. It seems to me that the difference in usefulness is probably due to their relative distance from common discourse.

pgustafs 6y ago

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.

spekcular 6y ago
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]. [1] https://en.wikipedia.org/wiki/Large_cardinal https://en.wikipedia.org/wiki/Large_cardinal

pgustafs 6y ago

We've hit the comment depth limit, so I'll reply here. > 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. Among other things, I want theorems about foundations to be useful to non-foundational mathematicians. Working on type theory can improve, at the very least, formal verification tools. In my view, traditional ZFC-based mathematical logic has a much smaller likelihood of being useful for regular mathematicians. For example, the vast majority of mathematicians will never explicitly assume the existence of a large cardinal in a paper. It seems to me that the difference in usefulness is probably due to their relative distance from common discourse.