Hacker News Reader

Comment by chas | Hacker News Reader

Homotopy type theory[1] is essentially working to show that math is (or can be viewed as) an interesting application of computer science.

[1] http://homotopytypetheory.org/2013/06/20/the-hott-book/

View on HN

Very interesting! I've often got into nasty arguments with people online when I dared to say that Computer science (Computing) was not a subset of math, but rather could be viewed more naturally as a superset. It is good to see serious academic work being done along these lines.

You can have the same debate about logic and mathematics, or to some extent philosophy and mathematics.

You could throw set theory into the ring as well :)

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.

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.

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.

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.

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.

HoTT even more than that. Type theory does what you describe without the "homotopy".

See: http://golem.ph.utexas.edu/category/2013/06/the_hott_book.ht...

It will be easier to convince mathematicians that homotopy theory is maths than it will be to convince them that type theory is (in general).

Reply on news.ycombinator.com