3 ms·

>In order to make these arguments less religious, I think it would be worthwhile to adopt Turing's mathematical philosophy, which called for adopting mathematic

>In order to make these arguments less religious, I think it would be worthwhile to adopt Turing's mathematical philosophy, which called for adopting mathematical foundations on an ad-hoc basis (or even no foundation at all). In other words, choose whatever foundation (if any) for the task at hand. This would make it easier to argue that, say, type theory is a more convenient core for proof checkers. I think you're misrepresenting the category theorists, they're usually the ones arguing for choosing whatever foundation is convenient for a given domain. A lot of the time, this is a type theoretic foundation because a lot of modern mathematics is about pretending you have function types when you don't actually have function types in your category (such as differential geometry) or that all you care about is a "core" set of operations and the rest of the framework you're working in simply gets in the way (such as Hilbert spaces vs. compact closed dagger categories in categorical quantum mechanics). And if you know already knew dependent type theory then synthetic homotopy theory is easier than classical homotopy theory, some proofs in homotopy theory can take several lectures to present and even then it will still be pretty hard to see why they hold. It's just weird to see people thing the category theorists are the one being impractical compared to the set theorists like Friedman. I can't think of a categorical logician who doesn't have an active line of research outside of logic; usually in topology, computability, quantum mechanics, or algebraic geometry. They're not just logicians but active researchers in computer science, physics and mathematics, logic is a powerful tool and should be applied in these fields.

pron 10y ago
I'm not trying to rule who is more reasonable (and frankly, I have no idea) and certainly not to misrepresent category theorists (whom I didn't mention), but just respond to fmap's statement that "ZFC itself is unnatural as a foundation for mathematics", which assumes that 1. a foundation is something is regularly used for anything, and 2. that it is something that is both fixed and essential for mathematics; in other words that the name "foundation", rather than signifying the study of math at the lowest levels, actually refers to something fundamental mathematics "rests on". Very little math is done on top of a formal foundation at all, and most of math does not even require a foundation. In fact, it is questionable whether any formal "foundations" are really foundational, or, as Wittgenstein called them, "just another calculus". If that is the case, it's meaningless to argue that ZFC isn't a natural foundation for mathematics, because in spite of the name, it may not really be a foundation at all; just another calculus that is called "foundational" because of its level of discourse, in which case the arguments against it can only be aesthetic or pragmatic. In order to be pragmatic, you need to say what for what uses the foundation is inadequate. But I think it's naive to pretend that there's no fight over aesthetics here, which is why I mentioned Turing, as I see a return to logicistic (as in logicism) arguments (which view mathematical foundations as truly fundamental) in new form, while Turing's philosophy manages to, according to Wittgenstein, avoid "needless dogmatism and dispute". I strongly encourage anyone interested in the subject to read Juliet Floyd's fascinating paper on Turing's mathematical philosophy: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf

pron 10y ago

I'm not trying to rule who is more reasonable (and frankly, I have no idea) and certainly not to misrepresent category theorists (whom I didn't mention), but just respond to fmap's statement that "ZFC itself is unnatural as a foundation for mathematics", which assumes that 1. a foundation is something is regularly used for anything, and 2. that it is something that is both fixed and essential for mathematics; in other words that the name "foundation", rather than signifying the study of math at the lowest levels, actually refers to something fundamental mathematics "rests on". Very little math is done on top of a formal foundation at all, and most of math does not even require a foundation. In fact, it is questionable whether any formal "foundations" are really foundational, or, as Wittgenstein called them, "just another calculus". If that is the case, it's meaningless to argue that ZFC isn't a natural foundation for mathematics, because in spite of the name, it may not really be a foundation at all; just another calculus that is called "foundational" because of its level of discourse, in which case the arguments against it can only be aesthetic or pragmatic. In order to be pragmatic, you need to say what for what uses the foundation is inadequate. But I think it's naive to pretend that there's no fight over aesthetics here, which is why I mentioned Turing, as I see a return to logicistic (as in logicism) arguments (which view mathematical foundations as truly fundamental) in new form, while Turing's philosophy manages to, according to Wittgenstein, avoid "needless dogmatism and dispute". I strongly encourage anyone interested in the subject to read Juliet Floyd's fascinating paper on Turing's mathematical philosophy: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf