7 ms·

The Foundations of Mathematics (2007) [pdf]

141 points by lainon 9y ago

eastWestMath 9y ago
I’m a category theorist so I’m going to nitpick - the claim that all concrete mathematical objects are specific sets is either tautological (a concrete category is literally one where each object has an underlying set) or untrue (I can think of several non-concrete categories that may be studied “concretely” using type theory, such as the microlinear spaces of synthetic differential geometry).
- danharaj 9y ago
  Non-commutative spaces are definitely not sets as well. That might have implications for foundations in the next century.
  - jimhefferon 9y ago
    I'd be interested to hear more. Any reference come to mind?
    - jesuslop 9y ago
      I'm liking https://arxiv.org/abs/math/0408416v1 https://arxiv.org/abs/math/0408416v1
- Verdex_3 9y ago
  Yeah, I would have thought that results like: https://www.scottaaronson.com/blog/?p=2725 https://www.scottaaronson.com/blog/?p=2725 show that set theory isn't the end all be all of mathematics.
  - ultrafilter 9y ago
    Every formal axiom system, whether about sets or anything else, can only prove that N of Busy Beavers halt, for some (not-too-large in practice) finite number N. If you just want to maximize N, right now your best bet is set theory plus a very strong large cardinal axiom, like I0. http://cantorsattic.info/L_of_V_lambda%2B1 http://cantorsattic.info/L_of_V_lambda%2B1 Perhaps simply because it is older, set theory is way ahead of its competitors in developing a hierarchy of extremely strong (but apparently consistent) axioms to supplement its base theory ZFC.
    - xamuel 9y ago
      You're confused. Only very basic arithmetic is needed to prove that any particular TM halts (if it does halt). You might have meant to say something like, "can only prove that N of the Busy Beavers are really Busy Beavers".
      - ultrafilter 9y ago
        You're right. I should have written "halts last among its peers" or similar.
espeed 9y ago
Isn't Vladimir Voevodsky's [1] Univalent Foundations [2] / Homotopy Type Theory [3] a new candidate challenging to subsume set theory as the foundations of mathematics [4]? [1] https://en.wikipedia.org/wiki/Vladimir_Voevodsky https://en.wikipedia.org/wiki/Vladimir_Voevodsky [2] https://en.wikipedia.org/wiki/Univalent_foundations https://en.wikipedia.org/wiki/Univalent_foundations [3] https://homotopytypetheory.org/ https://homotopytypetheory.org/ [4] https://www.youtube.com/results?search_query=Vladimir+Voevodsky+univalence+foundation+of+mathematics https://www.youtube.com/results?search_query=Vladimir+Voevod...
- kryptiskt 9y ago
  I wish people called these things "a foundation of mathematics" rather than "the foundation of mathematics". We have been able to pick and choose ever since foundations became a thing, and as long as they yield worthwhile results they're worthy objects of study. We don't have to pick one and stick with it, and it would be silly to classify stuff done with other axioms as non-mathematics.
  - ellius 9y ago
    I don’t disagree with you, but I think the human mind is essentially programmed to seek first causes. Part of what has made us so successful as a species is that we want to chase patterns down to their foundations, and I think it’s natural to feel that there is some “root” truth that explains the entirety of existence. I think that’s why a lot of people turn to simplistic unifying philosophies; it reduces a lot of intellectual anxiety if you have one big idea that subsumes all others, and upon which you can fall back when faced with uncomfortable questions. All of which is a long way of saying that while you’re correct, I think as a species we’ll always trend towards trying to find “THE foundation” even when the more rational thing is to “pick and choose” like you’re suggesting.
    - bohadi 9y ago
      An interesting thought brought to mind by your comments, our search for foundations (whether set theory, type theory, category theory, or higher order) reveals as much about our own minds as it does any idea of some external nature.
sahilbadal 9y ago
I think it is a necessary question to ask that what is mathematics which every serious student & teacher of mathematics should confront. The title of this book is “Foundations of Mathematics”, and there are a number of philosophical questions about this. However, the Foundations of Mathematics should give a precise deﬁnition of what a mathematical statement is and what a mathematical proof is.
- wastewaste 9y ago
  > the Foundations of Mathematics should give a precise deﬁnition of what a mathematical statement is and what a mathematical proof is. I don't see a difference between precise definition and mathematical statement in this context, so your question would be paradox. Is it wrong to ask though? I think higher logic is supposed to deal with these types of paradoxes. Your question, if taken rhetorical, is a statement about mathematical statements, a metapher. The in/-completeness theorems show that higher order logics like that are either inconsistent or incomplete. So a theory like you are asking for, is ab ever growing set of proofs that can't fit in a single book. Taken with a sense of philosophy in mind, a book can only be an introduction to think further. I was glad to read at least the intro to Univalent foundations mentioned in a previous comment. Russels paradox defies a set of all sets in first order logic. FOL is otherwise said to be complete, by the way, a fact often overlooked when talking about the related liars paradox. I was pleasently surprised to read that they just avoid the paradox by embedding theory into theory (Universes, tbh). To me that means we can't draw elemens from an arch-set, but have to build facts from the ground up.
fmap 9y ago
It's surprising that this was written in 2007. This article just perpetuates the tired old myth that there is something special about set theory... At its heart, set theory allows us to encode certain mathematical structures more or less naturally, but things are not "made out of sets". For example, the real numbers are not sets in the same sense that "the map is not the territory". Sets allow us to encode real numbers, but this encoding is mostly arbitrary. Is 3 an element of pi? If pi truly is a set, then this is a sensible question to ask, since sets are defined by their members. However, there is evidently an abstract concept of "real numbers" which exists without mentioning the elements of a real number. The technical reflection of this dilemma is the fact that in set theory there are multiple isomorphic copies of "the complete archimedean ordered field" which are all different as sets. This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. This might not matter so much for something as simple as a real number, but it matters a lot when you talk about more complicated structures.
- cpsempek 9y ago
  So, while type theory may have the benefit of resolving the "isomorphism issue" you describe, how is type theory not also another encoding of, for example, the real numbers?
- olfactory 9y ago
  > This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. Could you give a small example of how a simple bit of reasoning about a real (or even natural) number would work in both frameworks?
- mathsandphysics 9y ago
  Well, I wouldn't say type theory is superior. Real numbers can actually be logically constructed as sets. So yes, Pi is a set. For example, you can define the set of real numbers as the set of equivalent classes of rational cauchy sequences. In order words, Pi is a set of rational cauchy sequences that are equivalent (this set is infinite). In simple (non formal) words: Pi is the set of sequences of rational numbers that get closer and closer to the numerical value of Pi. >>>> Is 3 an element of pi? If pi truly is a set Pi being a set doesn't mean that it is a set of real numbers. In fact, that would be illogical (recursive). If Pi is a set, it must be a set of things that are not real numbers. So it is not logical to ask if 3 is an element of Pi. You can ask if 3 is equal to Pi, in which case the answer is no.
bumbledraven 9y ago
Related: Metamath (http://www.metamath.org http://www.metamath.org) is a tiny formal language for writing proofs in symbolic logic, as well as a tiny proof checker for the language. The author, Norm Megill, has used Metamath to formalize many theorems from set theory and analysis. For example, see his formalization of a typical proof that the square root of 2 is irrational: http://us.metamath.org/mpeuni/sqr2irr.html http://us.metamath.org/mpeuni/sqr2irr.html
unclesaamm 9y ago
This discussion seems like an apt place to drop Morris Kline's "Mathematics: The Loss of Certainty" (https://www.amazon.com/Mathematics-Loss-Certainty-Oxford-Paperbacks/dp/0195030850 https://www.amazon.com/Mathematics-Loss-Certainty-Oxford-Pap...). As a non-mathematician whose only exposure with a lot of these ideas is through that book, I can't help but see these discussions as falling very much in line with the competing schools of thought described in the book. The book is a non-academic tour of the history of mathematical foundations, and the way mathematicians struggled to rediscover "truth" or the purpose of their work when new crises were reached. For example, the book spends a good deal of time explaining the centrality of Euclidean geometry to people's worldviews, and the way that the discovery of non-Euclidean geometries shook people. Not just because they didn't assume other geometries could exist, but because people believed geometry to map onto Euclidean physical reality because it was God's way of revealing Himself to the world. The other main crises that the book toured were the discovery of quaternions, Cantor's theories, and Godel's theorem. Kline ends describing the arc over the last two hundred years of math as a splitting-off into four different schools: set theorists, intuitionists, formalists, and logicists. Each camp tried to reassert math on "solid ground". I hear echos of those debates in this thread, where some are asserting that there can possibly exist multiple foundations, which from my reading of the book is a very formalist idea (our rules of math are a formal system, and any internally consistent set of rules are just as valid as objects of study). Not being a mathematician, I don't have a sense of where those schools played out to the current day. I'd be curious to hear if they're all still around in different forms, or whether some have more or less died out.

141 points by lainon 9y ago

I’m a category theorist so I’m going to nitpick - the claim that all concrete mathematical objects are specific sets is either tautological (a concrete category is literally one where each object has an underlying set) or untrue (I can think of several non-concrete categories that may be studied “concretely” using type theory, such as the microlinear spaces of synthetic differential geometry).

danharaj 9y ago
Non-commutative spaces are definitely not sets as well. That might have implications for foundations in the next century.
- jimhefferon 9y ago
  I'd be interested to hear more. Any reference come to mind?
  - jesuslop 9y ago
    I'm liking https://arxiv.org/abs/math/0408416v1 https://arxiv.org/abs/math/0408416v1
Verdex_3 9y ago
Yeah, I would have thought that results like: https://www.scottaaronson.com/blog/?p=2725 https://www.scottaaronson.com/blog/?p=2725 show that set theory isn't the end all be all of mathematics.
- ultrafilter 9y ago
  Every formal axiom system, whether about sets or anything else, can only prove that N of Busy Beavers halt, for some (not-too-large in practice) finite number N. If you just want to maximize N, right now your best bet is set theory plus a very strong large cardinal axiom, like I0. http://cantorsattic.info/L_of_V_lambda%2B1 http://cantorsattic.info/L_of_V_lambda%2B1 Perhaps simply because it is older, set theory is way ahead of its competitors in developing a hierarchy of extremely strong (but apparently consistent) axioms to supplement its base theory ZFC.
  - xamuel 9y ago
    You're confused. Only very basic arithmetic is needed to prove that any particular TM halts (if it does halt). You might have meant to say something like, "can only prove that N of the Busy Beavers are really Busy Beavers".
    - ultrafilter 9y ago
      You're right. I should have written "halts last among its peers" or similar.

espeed 9y ago

Isn't Vladimir Voevodsky's [1] Univalent Foundations [2] / Homotopy Type Theory [3] a new candidate challenging to subsume set theory as the foundations of mathematics [4]? [1] https://en.wikipedia.org/wiki/Vladimir_Voevodsky https://en.wikipedia.org/wiki/Vladimir_Voevodsky [2] https://en.wikipedia.org/wiki/Univalent_foundations https://en.wikipedia.org/wiki/Univalent_foundations [3] https://homotopytypetheory.org/ https://homotopytypetheory.org/ [4] https://www.youtube.com/results?search_query=Vladimir+Voevodsky+univalence+foundation+of+mathematics https://www.youtube.com/results?search_query=Vladimir+Voevod...

kryptiskt 9y ago
I wish people called these things "a foundation of mathematics" rather than "the foundation of mathematics". We have been able to pick and choose ever since foundations became a thing, and as long as they yield worthwhile results they're worthy objects of study. We don't have to pick one and stick with it, and it would be silly to classify stuff done with other axioms as non-mathematics.
- ellius 9y ago
  I don’t disagree with you, but I think the human mind is essentially programmed to seek first causes. Part of what has made us so successful as a species is that we want to chase patterns down to their foundations, and I think it’s natural to feel that there is some “root” truth that explains the entirety of existence. I think that’s why a lot of people turn to simplistic unifying philosophies; it reduces a lot of intellectual anxiety if you have one big idea that subsumes all others, and upon which you can fall back when faced with uncomfortable questions. All of which is a long way of saying that while you’re correct, I think as a species we’ll always trend towards trying to find “THE foundation” even when the more rational thing is to “pick and choose” like you’re suggesting.
  - bohadi 9y ago
    An interesting thought brought to mind by your comments, our search for foundations (whether set theory, type theory, category theory, or higher order) reveals as much about our own minds as it does any idea of some external nature.

sahilbadal 9y ago

I think it is a necessary question to ask that what is mathematics which every serious student & teacher of mathematics should confront. The title of this book is “Foundations of Mathematics”, and there are a number of philosophical questions about this. However, the Foundations of Mathematics should give a precise deﬁnition of what a mathematical statement is and what a mathematical proof is.

wastewaste 9y ago
> the Foundations of Mathematics should give a precise deﬁnition of what a mathematical statement is and what a mathematical proof is. I don't see a difference between precise definition and mathematical statement in this context, so your question would be paradox. Is it wrong to ask though? I think higher logic is supposed to deal with these types of paradoxes. Your question, if taken rhetorical, is a statement about mathematical statements, a metapher. The in/-completeness theorems show that higher order logics like that are either inconsistent or incomplete. So a theory like you are asking for, is ab ever growing set of proofs that can't fit in a single book. Taken with a sense of philosophy in mind, a book can only be an introduction to think further. I was glad to read at least the intro to Univalent foundations mentioned in a previous comment. Russels paradox defies a set of all sets in first order logic. FOL is otherwise said to be complete, by the way, a fact often overlooked when talking about the related liars paradox. I was pleasently surprised to read that they just avoid the paradox by embedding theory into theory (Universes, tbh). To me that means we can't draw elemens from an arch-set, but have to build facts from the ground up.

fmap 9y ago

It's surprising that this was written in 2007. This article just perpetuates the tired old myth that there is something special about set theory... At its heart, set theory allows us to encode certain mathematical structures more or less naturally, but things are not "made out of sets". For example, the real numbers are not sets in the same sense that "the map is not the territory". Sets allow us to encode real numbers, but this encoding is mostly arbitrary. Is 3 an element of pi? If pi truly is a set, then this is a sensible question to ask, since sets are defined by their members. However, there is evidently an abstract concept of "real numbers" which exists without mentioning the elements of a real number. The technical reflection of this dilemma is the fact that in set theory there are multiple isomorphic copies of "the complete archimedean ordered field" which are all different as sets. This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. This might not matter so much for something as simple as a real number, but it matters a lot when you talk about more complicated structures.

cpsempek 9y ago
So, while type theory may have the benefit of resolving the "isomorphism issue" you describe, how is type theory not also another encoding of, for example, the real numbers?
olfactory 9y ago
> This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. Could you give a small example of how a simple bit of reasoning about a real (or even natural) number would work in both frameworks?
mathsandphysics 9y ago
Well, I wouldn't say type theory is superior. Real numbers can actually be logically constructed as sets. So yes, Pi is a set. For example, you can define the set of real numbers as the set of equivalent classes of rational cauchy sequences. In order words, Pi is a set of rational cauchy sequences that are equivalent (this set is infinite). In simple (non formal) words: Pi is the set of sequences of rational numbers that get closer and closer to the numerical value of Pi. >>>> Is 3 an element of pi? If pi truly is a set Pi being a set doesn't mean that it is a set of real numbers. In fact, that would be illogical (recursive). If Pi is a set, it must be a set of things that are not real numbers. So it is not logical to ask if 3 is an element of Pi. You can ask if 3 is equal to Pi, in which case the answer is no.

bumbledraven 9y ago

Related: Metamath (http://www.metamath.org http://www.metamath.org) is a tiny formal language for writing proofs in symbolic logic, as well as a tiny proof checker for the language. The author, Norm Megill, has used Metamath to formalize many theorems from set theory and analysis. For example, see his formalization of a typical proof that the square root of 2 is irrational: http://us.metamath.org/mpeuni/sqr2irr.html http://us.metamath.org/mpeuni/sqr2irr.html

unclesaamm 9y ago

This discussion seems like an apt place to drop Morris Kline's "Mathematics: The Loss of Certainty" (https://www.amazon.com/Mathematics-Loss-Certainty-Oxford-Paperbacks/dp/0195030850 https://www.amazon.com/Mathematics-Loss-Certainty-Oxford-Pap...). As a non-mathematician whose only exposure with a lot of these ideas is through that book, I can't help but see these discussions as falling very much in line with the competing schools of thought described in the book. The book is a non-academic tour of the history of mathematical foundations, and the way mathematicians struggled to rediscover "truth" or the purpose of their work when new crises were reached. For example, the book spends a good deal of time explaining the centrality of Euclidean geometry to people's worldviews, and the way that the discovery of non-Euclidean geometries shook people. Not just because they didn't assume other geometries could exist, but because people believed geometry to map onto Euclidean physical reality because it was God's way of revealing Himself to the world. The other main crises that the book toured were the discovery of quaternions, Cantor's theories, and Godel's theorem. Kline ends describing the arc over the last two hundred years of math as a splitting-off into four different schools: set theorists, intuitionists, formalists, and logicists. Each camp tried to reassert math on "solid ground". I hear echos of those debates in this thread, where some are asserting that there can possibly exist multiple foundations, which from my reading of the book is a very formalist idea (our rules of math are a formal system, and any internally consistent set of rules are just as valid as objects of study). Not being a mathematician, I don't have a sense of where those schools played out to the current day. I'd be curious to hear if they're all still around in different forms, or whether some have more or less died out.