[davorak]

I did not get the impression, from the blog posts, that HOTT was putting forth that CS could or is a super set of math just that it can be used as a foundation for all mathematics, just like set theory or category theory can be.

[hackinthebochs]

I think this is where terminology breaks down a bit, but my reading of "basis of" is taken as being loosely equivalent to saying a superset of. In this same sense, logic can be seen as the basis for all mathematics. Anything that is math is also strictly logic, hence math is a subset of logic.

[SatvikBeri]

This is a fairly interesting philosophical question. Personally I view (and use) Math as a set of abstractions to understand the world, and use Mathematical Logic to help make Math more rigorous and proofs more checkable. But if it turned out that Mathematical Logic had some flaws as it is formalized today, I wouldn't throw out Probability Theory or Algebra. Instead I would seek a formalization of Mathematical Logic that made those things useful.

I don't think that there's any formal system you can use as the basis of all Math, though. For example, ZFC can't talk about proper classes, but we'd like to be able to make statements about the class of all sets, and the collection of all classes, etc.

[cwzwarich]

Mathematics existed long before logic came to explain it, and most practicing mathematicians don't care that much about formal logic or think about it in their day-to-day work. The incompleteness theorems add a further disconnect.

[hackinthebochs]

I don't think it makes sense to say one can do mathematics without logic. Even if early math users didn't have a concept of formal logic, their mathematical reasoning was still dependent on it.