5 ms·
> vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle I think this is the basis for the enthusiasm, a
by andrewla 6y ago
> vehicle for doing mathematics with intuitionistic logic, and in particular denying the law of excluded middle
I think this is the basis for the enthusiasm, almost entirely. There's a growing perception that a lot of mathematical abstractions that are purely naval-gazing have arisen from ZFC, and the intuitionalists and finitists are gaining followers amongst amateur and upcoming mathematicians. I don't have data to back this, just a feeling that I get.
And I think in particular this is attractive to programmers because this skews closer to what we've learned about computability and program design, and I think there's even some hope of moving forward from obscure notation and single-letter variable names towards a syntax for doing mathematics that can be more expressive and easier to verify.
- boyobo 6y agoYou don't need anything like HoTT to start using multi-letter variable names. E.g. https://mitpress.mit.edu/books/functional-differential-geometry https://mitpress.mit.edu/books/functional-differential-geome...
- foxes 6y agoI just had a flip through this book, yes all the differential geometry is there, but I think its a bit of a let down. If I think "functional" I want to think more abstractly in terms of categories, functors, functions. The Lisp code in this book is truly not doing anything for me. Seems like a kind of direct numerical computation/translation. I actually think it would be better to do it in Haskell which seems like it would at least let you identify some more generic structures (oh we can actually implement this idea x as a functor/monad blah blah).
- taliesinb 6y agoCouldn’t agree more. A great example of a mathematics popularizer along these lines is Norman Wildberger, who has an astonishing range of videos on youtube about an amazing range of mathematical topics. Here’s an interview with him: https://youtu.be/E_dGqavx5AU https://youtu.be/E_dGqavx5AU . My personal feeling is that a lot of beautiful and interesting mathematics will arise as a result of an intuitionist, finitist, computationalist rethinking of the foundations of mathematics.
- auggierose 6y agoI am not sure HoTT is your best bet if you want to get away from obscure notation and naval-gazing. Just kidding. But seriously, ZFC is probably the easiest foundation you can have for proper mathematics. Anything else is more complicated (if you think otherwise, you probably just don't understand it).