Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I never said "set theory is not rigorous." Euclid wrote Elements without knowing anything about set theory. Math was done for thousands of years without modern set theory or any modern notion of logical foundations. Set theory is more rigorous than what came before it.

It's not as rigorous as type theory (yes, this is an umbrella term) because type theory can be verified by a computer. Homotopy type theory is an example of the type of math that set theory can't handle

There are so many layers of ignorance to unpack here and I don't care to be your unpaid tutor



> because type theory can be verified by a computer

proofs in FOL can be checked by a computer without any need for type theory - just look at metamath.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: