7 ms·

There is a lot of ordinary mathematics that is outside of ZFC, which Friedman is well aware of but the writer of this article may not be. Grothendieck was not i

by fmap 10y ago

There is a lot of ordinary mathematics that is outside of ZFC, which Friedman is well aware of but the writer of this article may not be. Grothendieck was not interested in abstract set theory when he introduced what are now called "Grothendieck Universes". He merely wanted to do algebraic geometry at a high level of abstraction. Similarly, Conway was apparently a bit dismayed when the formalization of his simple idea of "surreal numbers" required deeply unnatural encodings in ZFC... My opinion is still that ZFC itself is unnatural as a foundation for mathematics, precisely because we have to do so much encoding to get anything useful out of it. And whenever you iterate "large" encodings you leave the universe of "ordinary ZFC". Conway suggested - and this is realized in modern type theory - that we should instead allow arbitrary "free" constructions, such as his surreal numbers, to extend the basic universe of mathematics. To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals. This is not a direction that Friedman considers worthwhile, because he thinks that first-order logic and ZFC are inevitable. It's a shame that so many people on the FOM mailing list share the same view. There are good reasons why you don't find a lot of category theorists on that list anymore...

auggierose 10y ago
You can combine ZFC and simple type theory to give you something in which you can comfortably do surreal numbers. This is done by embedding ZFC as a simple type. For example, here this is done for Partizan Games (which contain the surreal numbers): http://link.springer.com/chapter/10.1007/11921240_19 http://link.springer.com/chapter/10.1007/11921240_19
sanduu 10y ago
Do you use a pay~pal ? because if you do you can include an extra 300 a week to your earnings only working on the internet for 5 hours per day, check this site... http://bit.ly/2atnA1a http://bit.ly/2atnA1a
pron 10y ago
> a lot of ordinary mathematics that is outside of ZFC A lot of ordinary math? I think there's one if not two exaggerations in there. > My opinion is still that ZFC itself is unnatural as a foundation for mathematics, precisely because we have to do so much encoding to get anything useful out of it. One of the things Friedman likes to emphasize about the foundation of math is that there is very little you actually need to do with it. A good foundation is one that you don't even need to know is there. Most mathematicians don't work in any formalism, so a foundation doesn't need to be useful. It's not as if anyone actually needs to do all those tedious set encodings. Except that many of those who call for new foundations are really interested in mechanical proof checkers, and those do have to be useful. 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. > This is not a direction that Friedman considers worthwhile, because he thinks that first-order logic and ZFC are inevitable. That's not how I read him. He thinks that FOL and ZFC are good enough, and as foundations don't matter in practice (a good foundation is one you can ignore; I think that's a quote by him), it would take some achievement to justify seriously considering alternatives. He even says what it would take: easier teaching and/or easier proofs. So far no alternative foundation has been able to improve either one.
- hyperpape 10y ago
  Algebraic geometry seems entirely like ordinary math, in the funny sense where it doesn't mean "elementary" but "the kind of thing mathematicians who don't intrinsically care about foundations like to do".
- eastWestMath 10y ago
  >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
nuncanada 10y ago
Precisely. Any attempts of even discussion about Higher Order theories on that list ends up with Harvey stating something that can be translated to those without the technical expertise as "Every higher order theory is a first order theory in disguise". Which is true but besides the point. Just look at Peano's axiomatization of the Natural Numbers and perceive how intuitively bad it is at abstracting what Natural Numbers are. He constructs an "ugly" object that is isomorphic to Natural Numbers, but doesn't correspond to what Mathematicians intuitively believe the Natural Numbers to be. With a Second Order theory you can just axiomatize the Natural Number in a pretty straightforward way that correspond to Mathematician's intuition about the Set...
- Pete_D 10y ago
  At the risk of asking a naïve question, why do you think the Peano axioms are ugly? As a mostly-lay mathematician I always thought they were quite elegant.
  - Kutta 10y ago
    My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already corresponds very closely to intuitions about intended (standard) models. In contrast, the lack of clear computational meaning in classical theories makes it necessary find philosophical justifications, which in turn usually refer to other theories without clear computational meaning. Of course, we can compile classical proofs to programs as well through a variety of transformations, but they tend to be sort of unsatisfying, for example we may get functions with empty domains that we can't actually call, instead of programs evaluating to numerals. So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers, rather statements referring to things which have properties which we think numbers should have. And then we can choose between sticking to first-order logic and leaving non-standard models in, or switching to second-order induction which lets us prove more statements at the cost of completeness and leaning more on ambient set theory. Simpson seems to be critical of second-order logic because it's set theory in disguise; but to me that kind of dispute is moot because I find any sort of classical logic unsuitable for mathematical foundations.
deleted 10y ago
[deleted]
lgandersen 10y ago
> To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals. I don't see why the size of Mahlo cardinals is ridiculous. Considering all the strongly inaccessible cardinals that have been discovered, Mahlo cardinals is rather weak. Also, the definition of a Grothendieck universe strongly resembles the definition of a strongly inaccessible cardinal, imho. That they are equivalent are (relatively) straightforward. Harvey Friedmans work on provable equivalences between large cardinals way larger than Mahlo cardinals and theorems about objects in the domain of the rationals further substantiates this. Very fascinating.
- fmap 10y ago
  What do you mean exactly? Grothendieck universes correspond to the some inaccessible cardinals, but the axiom that every set is contained in a Grothendieck universe (which is stronger than just saying that there are omega-many inaccessible cardinals of increasing size) is itself weaker than the existence of a single Mahlo cardinal... And (afaik) you need a Mahlo cardinal for every type theoretic universe that is closed under induction-recursion. My point is that induction-recursion is a very intuitive notion from a computational perspective, yet its encoding in set theory is anything but intuitive...

by fmap 10y ago

auggierose 10y ago

You can combine ZFC and simple type theory to give you something in which you can comfortably do surreal numbers. This is done by embedding ZFC as a simple type. For example, here this is done for Partizan Games (which contain the surreal numbers): http://link.springer.com/chapter/10.1007/11921240_19 http://link.springer.com/chapter/10.1007/11921240_19

sanduu 10y ago

Do you use a pay~pal ? because if you do you can include an extra 300 a week to your earnings only working on the internet for 5 hours per day, check this site... http://bit.ly/2atnA1a http://bit.ly/2atnA1a

pron 10y ago

> a lot of ordinary mathematics that is outside of ZFC A lot of ordinary math? I think there's one if not two exaggerations in there. > My opinion is still that ZFC itself is unnatural as a foundation for mathematics, precisely because we have to do so much encoding to get anything useful out of it. One of the things Friedman likes to emphasize about the foundation of math is that there is very little you actually need to do with it. A good foundation is one that you don't even need to know is there. Most mathematicians don't work in any formalism, so a foundation doesn't need to be useful. It's not as if anyone actually needs to do all those tedious set encodings. Except that many of those who call for new foundations are really interested in mechanical proof checkers, and those do have to be useful. 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. > This is not a direction that Friedman considers worthwhile, because he thinks that first-order logic and ZFC are inevitable. That's not how I read him. He thinks that FOL and ZFC are good enough, and as foundations don't matter in practice (a good foundation is one you can ignore; I think that's a quote by him), it would take some achievement to justify seriously considering alternatives. He even says what it would take: easier teaching and/or easier proofs. So far no alternative foundation has been able to improve either one.

hyperpape 10y ago
Algebraic geometry seems entirely like ordinary math, in the funny sense where it doesn't mean "elementary" but "the kind of thing mathematicians who don't intrinsically care about foundations like to do".
eastWestMath 10y ago
>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

nuncanada 10y ago

Precisely. Any attempts of even discussion about Higher Order theories on that list ends up with Harvey stating something that can be translated to those without the technical expertise as "Every higher order theory is a first order theory in disguise". Which is true but besides the point. Just look at Peano's axiomatization of the Natural Numbers and perceive how intuitively bad it is at abstracting what Natural Numbers are. He constructs an "ugly" object that is isomorphic to Natural Numbers, but doesn't correspond to what Mathematicians intuitively believe the Natural Numbers to be. With a Second Order theory you can just axiomatize the Natural Number in a pretty straightforward way that correspond to Mathematician's intuition about the Set...

Pete_D 10y ago
At the risk of asking a naïve question, why do you think the Peano axioms are ugly? As a mostly-lay mathematician I always thought they were quite elegant.
- Kutta 10y ago
  My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already corresponds very closely to intuitions about intended (standard) models. In contrast, the lack of clear computational meaning in classical theories makes it necessary find philosophical justifications, which in turn usually refer to other theories without clear computational meaning. Of course, we can compile classical proofs to programs as well through a variety of transformations, but they tend to be sort of unsatisfying, for example we may get functions with empty domains that we can't actually call, instead of programs evaluating to numerals. So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers, rather statements referring to things which have properties which we think numbers should have. And then we can choose between sticking to first-order logic and leaving non-standard models in, or switching to second-order induction which lets us prove more statements at the cost of completeness and leaning more on ambient set theory. Simpson seems to be critical of second-order logic because it's set theory in disguise; but to me that kind of dispute is moot because I find any sort of classical logic unsuitable for mathematical foundations.

deleted 10y ago

[deleted]

lgandersen 10y ago

> To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals. I don't see why the size of Mahlo cardinals is ridiculous. Considering all the strongly inaccessible cardinals that have been discovered, Mahlo cardinals is rather weak. Also, the definition of a Grothendieck universe strongly resembles the definition of a strongly inaccessible cardinal, imho. That they are equivalent are (relatively) straightforward. Harvey Friedmans work on provable equivalences between large cardinals way larger than Mahlo cardinals and theorems about objects in the domain of the rationals further substantiates this. Very fascinating.

fmap 10y ago
What do you mean exactly? Grothendieck universes correspond to the some inaccessible cardinals, but the axiom that every set is contained in a Grothendieck universe (which is stronger than just saying that there are omega-many inaccessible cardinals of increasing size) is itself weaker than the existence of a single Mahlo cardinal... And (afaik) you need a Mahlo cardinal for every type theoretic universe that is closed under induction-recursion. My point is that induction-recursion is a very intuitive notion from a computational perspective, yet its encoding in set theory is anything but intuitive...