5 ms·
I understand your last sentence to agree with the statement that everything could be formalized in ZFC given sufficient effort. (I do not really care by what me
by spekcular 4y ago
I understand your last sentence to agree with the statement that everything could be formalized in ZFC given sufficient effort. (I do not really care by what means we know this can be done.) If so, then I'm not sure why you disagree with what I wrote previously.
- zozbot234 4y ago> everything could be formalized in ZFC given sufficient effort Since I'm not sure what could be comprised under "everything", I don't think I can agree with that statement. The whole point of "practical" formalization efforts is to add some rigor to such assertions. And you've acknowledged that type theoretical foundations can be useful to practitioners, so what's it exactly that you disagree about?
- spekcular 4y agoThe disagreement is about whether there are reasons aside from facilitating formalization to care about HoTT. (Because if not, it seems like we should all be jumping on the Lean bandwagon instead.)