9 ms·

100 years of Zermelo's axiom of choice: What was the problem with it? (2006)

122 points by Bogdanp 1y ago

deleted 1y ago
[deleted]
math_comment_21 1y ago
In topology, if you have a continuous surjective map X --> Y, then it might have a continuous splitting (a map the other way which is a "partial" inverse in the sense that Y ---> X ---> Y is the identity) e.g. there are lots of splittings of the projection R^2 ---> R, you could include the line back as the x-axis but also the graph of any continuous function is a splitting. On the other hand, there's no continuous splitting of the map from the unit interval to the circle that glues together the two endpoints. So the category of topological spaces does not have the property "every epimorphism splits." As the article mentions, the axiom of choice says that the category of sets has this property. So we can think of the various independence results of the 20th century as saying, hey, (assuming ZFC is consistent) there's this category, Set, with this rule, and there's this other category called idk Snet, that satisfies the ZF axioms but where there are some surjections that don't split, and that's ok too. Then whatever, if you want to study something like rings but you don't like the axiom of choice, define a rning to be a snet with two binary operations such that blah blah blah, and you've got a nice category Rning and your various theorems about rnings and maybe they don't all have maximal ideals, even though rings do. You're not arguing about ontology or the nature of truth, you're just picking which category to work in.
- karmakurtisaani 1y ago
  Yeah, it's important to think of these axioms as choosing the rules of the game, rather than what intuitively makes sense. The real question is if playing the game produces useful results.
  - btilly 1y ago
    Spoken like a true formalist. It doesn't really have to mean anything when we say that the reals are a larger set than the natural numbers - that's just the conclusion of the game that we are playing. What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
    - skissane 1y ago
      > What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with? The claim that there are more reals than naturals holds given classical ZF(C) set theory. But there are alternative set theories in which the reals are countable, e.g. NFU+AxCount. These alternative set theories ensure all reals are countable by rendering Cantor’s diagonalisation argument invalid, since their axioms are too weak to validate it. But, they contain all the same reals as the high school mathematics concept of “reals”. So, there are many reals, and that some of them are countable and others are not are indeed “eternal truths” (it is an eternal truth that whatever axioms have the consequences they do), but the everyday (non-expert) concept of reals isn’t any of them in particular - and it is unclear if the dominance of classical notions in mainstream professional mathematics was historically inevitable or a historical accident - maybe, on the other side of the galaxy, there exists some alien civilisation, in which different foundations of mathematics are mainstream, because their mathematics took a different evolutionary course from ours - maybe for them, reals are classically countable, and uncountability is an exotic notion belonging to alternative foundations of mathematics
      - btilly 1y ago
        As I pointed out at https://news.ycombinator.com/item?id=44271589 https://news.ycombinator.com/item?id=44271589, there are systems that can accept Cantor's argument, without concluding that there are more reals than rational numbers. As you point out, there are many mathematical systems that contain all of the numbers in the high school mathematics concept of "reals". Since those with a high school understanding of reals do not know which of those systems they would agree with, they should not be asked to accept as true, any results that hold in only some of those systems. And that is why I don't like mathematicians telling lay audiences that there are more reals than rationals.
  - woopsn 1y ago
    Axioms are also introduced in practical terms just to make proofs and results "better". Usually we talk in terms of what propositions are provable, saying that indicates the strength/power of these assumptions, but beyond this there are issues of proof length and complexity. For example in arithmetic without induction, roughly, theorems remain the same (those which can still be expressed) but may have exponentially longer proofs because of the loss of those `∀n P(n)`-type propositions. In this sense it does sometimes come back to intuition. If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition and doesn't really change "the game" we are trying to play. It just makes it more intuitive and playable.
    - karmakurtisaani 1y ago
      Good point. I would argue, however, that having nicer proofs is a "useful" result of the game.
    - SabrinaJewson 1y ago
      I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545 https://math.stackexchange.com/a/4076545): - ℕ ∪ {∞} - Cardinal arithmetic - ℤ[x]⁺ Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way. I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).
      - deleted 1y ago
        [deleted]
      - woopsn 1y ago
        If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.
- alexey-salmin 1y ago
  Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.
  - gsf_emergency 1y ago
    Careful here, you might wake up the diabol (of pure algebra)
  - pfortuny 1y ago
    Yes, but the parent comment is trying to say "imagine the world would only be made up of topological spaces and continuous maps". Then the retraction principle would not hold.
- LudwigNagasena 1y ago
  How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.
  - gylterud 1y ago
    Category theory gives a structural framework for discussing these things. The various categories live side by side and can be related with functors. This allows a broader view and makes it easier perhaps, to understand that there isn’t a right answer to “what is true” about sets in the absolute.
    - LudwigNagasena 1y ago
      But then you would think there is a right answer to “what is true” about categories, and you would face AC again.
      - gylterud 1y ago
        For sure there would have to be a meta theory of some sort. But, I think that many classical mathematicians would be happy with that meta theory to be weaker, rather than stronger. I don't think there is a need for that theory to have AC. After all, thanks to its independence of from the other axioms, AC does not add logical strength to a classical theory. (For die-hard constructivists, such as myself, the story is of course different. But that story is for a another time. I am presenting the classical view here.)
mietek 1y ago
Author of the mechanization here. Feel free to suggest materials from the history of intuitionistic mathematics and type theory that ought to be mechanized and made available to a wider audience — the less well-known, the better.
- btilly 1y ago
  I wish that I had specific suggestions. My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist. (By internet coincidence, I recently wrote https://math.stackexchange.com/questions/5074503/can-pa-prove-each-goodstein-sequence-can-be-proven-in-pa-to-reach-zero/5075056#5075056 https://math.stackexchange.com/questions/5074503/can-pa-prov... which ends with the beginning of the construction of that list, starting with the Peano axioms. https://news.ycombinator.com/item?id=44269822 https://news.ycombinator.com/item?id=44269822 is about that answer.) Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with. I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it. All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.
  - Jtsummers 1y ago
    A nit, but: > Strictly speaking, a programming language doesn't really need comments. "But Lisp has them, and puts them in double quotes." Lisp has comments, but they aren't generally contained in double quotes, you've tossed a lot of strings into your program and called them comments. Comments are either marked with ; (comment to end of line, like //) with conventions on how many semicolons to use in particular places, or comment blocks with #| comment |# (nestable version of /* */). You can add documentation to many definitions, like functions, using strings which may be what you're thinking of but that happens inside the definition like with this: (defun constant (x) "CONSTANT returns a function which always returns X" (lambda (a) x)) Which is a comment, but it's unusual to use strings as comments outside of contexts like that. Also, if you're going to use strings as comments you can make them multi-line instead of doing "I thought about calling these car and cdr..." "...then decided that I'm not really THAT addicted to Lisp" with: "I thought about calling these car and cdr... ...then decided that I'm not really THAT addicted to Lisp" The other reason I'm posting this nit is that if anyone reads your blog/answer and tries to use comments as you've described them inside of expressions they'll be very confused about why it's behaving incorrectly. There's no reason to mislead people, this is not a comment: (if (= 1 2) "Should never be true" ;; that's not a comment, it's an expression (print "Never happens") (print "Always happens")) ;; your interpreter or compiler will complain about this code
jasperry 1y ago
So if I understand the claim of this correctly (I'm a spectator of logic research and haven't tried to follow the proofs), there is a constructive version of AoC that is obviously true, but it's not the same as Zermelo's axiom because that one is extensional. Zermelo's axiom can be formulated in constructive mathematics but gives you things you don't want (like excluded middle.) Is this close to a correct statement of the paper's result? Is all this agreed on today? Have there been any significant refinements?
- ncfavier 1y ago
  That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from. The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8). Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.
  - creata 1y ago
    Off-topic: What's the state of homotopy type theory as an alternative foundation for mathematics? Has it been used to simplify any proofs or prove anything new?
    - zozbot234 1y ago
      Kevin Buzzard (a standard mathematician who has direct expertise in the sorts of things HoTT is supposed to help with) argues that we simply don't know yet. See the references I previously mentioned in https://news.ycombinator.com/item?id=44151283 https://news.ycombinator.com/item?id=44151283
impostervt 1y ago
I've never quite gotten the axiom of choice. Can anyone ELI5?
- bobbylarrybobby 1y ago
  The Cartesian product of nonempty sets is nonempty. This is obvious!, you might say — obviously we can just pick one element from each set and be done with it. But the statement that we can pick an element from each set is the axiom of choice. Note that it's not necessarily simple to pick an element from a set. For instance, how would one pick an element from the set of uncomputable numbers? A human cannot describe said element, by definition. The axiom of choice says it's possible anyway.
  - deleted 1y ago
    [deleted]
  - throw310822 1y ago
    Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
    - littlestymaar 1y ago
      As far as I understand there's no such thing “undecidable” in absolute, Gödel incompleteness theorem is about being undecidable under a certain set of axioms.
  - moefh 1y ago
    > A human cannot describe said element, by definition. That example doesn't work. Some numbers are describable but not computable, Chaitin's constant being the famous example: https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Chaitin%27s_constant
    - deleted 1y ago
      [deleted]
scoofy 1y ago
[flagged]
- ptero 1y ago
  Axioms should capture the rules we can assume without justification. But in most cases we want them to reflect the rules of the real world in the sense that statements derived from those axioms reflect our observations. That part (reflect observations) can be separated by many levels of abstractions, etc. I would not try visualizing general statements on Lie algebras or spectral theorems, but those abstractions serve the same goal -- help derive conclusions that apply in the real world. My 2c.
  - simion314 1y ago
    It is not about real world, choosing an axiom set must simply put produce something valid (with no contradictions) and that is not trivial.
    - dist-epoch 1y ago
      Math is done backwards. We know what kind of results we want to be true, and then we search for the minimum number of axioms which can deliver that.
      - woopsn 1y ago
        There is another goal in addition to minimizing the number/complexity of axioms. Some "axioms" like induction actually introduce an infinite family of assumptions, a so-called schema. So in addition to working backwards from our (incomplete) knowledge, we find certain axioms let us make arguments that are obviously valid but would be formally very tedious without them.
    - ptero 1y ago
      Some math is not about the real world. This is not my kettle of fish, but I have heard of some general topology research directions that discusses properties of topological spaces that probably do not exist at all. Those (according to a friend whose advisor worked in the area) are pretty sad affairs, with only 5-10 people in the world who understand or care about this particular sliver of the math. But some math is about providing tools (again, likely via levels of abstractions) for understanding the world and, to me, this is the "real math". This is a personal view, not an absolute position. I started on the other side of this fence and during my pure math PhD regularly picked fights with our buddies doing physics PhD arguing that mathematics is self-sufficient and does not need any validation from other sciences. But over the next 30 years gradually went to the other side and now think that my original view leads to splintering into gazillion tiny slivers that do not care about anything else; not even about adjacent slivers. Which leads to degeneration. My 2c.
munificent 1y ago
The material is way over my head, but, wow, what a beautifully designed page. The layout and typography is delightful.
- deleted 1y ago
  [deleted]
- mietek 1y ago
  Thanks! The source code is set in Fabrizio Schiavi’s amazing PragmataPro. https://fsd.it/shop/fonts/pragmatapro/ https://fsd.it/shop/fonts/pragmatapro/ https://github.com/fabrizioschiavi/pragmatapro https://github.com/fabrizioschiavi/pragmatapro
CliffStoll 1y ago
And the Axiom of Choice implies the Banach-Tarski parodox. It's anti-intuitive: Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun.
- dist-epoch 1y ago
  The number of pieces is finite, but each piece consists of an infinite number of scattered points: > However, the pieces themselves are not "solids" in the traditional sense, but infinite scatterings of points.
- tweakimp 1y ago
  Can you really reassemble them into something bigger or just into more copies of the same size?
- nwallin 1y ago
  > Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun. "Finite number of pieces" is a tricky thing. It's a finite number of pieces, sure, but each of those pieces is made of an uncountably infinite number of pieces. Banach-Tarski is a clever way of sweeping an infinite number of dust bunnies under the rug until just the right moment, when it reveals all infinitely many of them in the shape of a pea and claims to have just created them, when in reality, they were actually there all along, hiding under the rug. For me, Banach-Tarski is just an another version of Hilbert's Hotel, but with uncountable infinities instead of countable ones. Once you accept, in your heart, that infinity is real and is equally deserving of your love and respect as finite natural numbers, then the paradoxicalness of Banach-Tarski melts away.
- fpoling 1y ago
  Essentially the axiom of choice allows for 3-d sets that do not preserve their volume upon rotation/movement. Such sets, of cause, cannot be constructed or even described as their description will contain infinite number of steps.
revskill 1y ago
[flagged]
jfengel 1y ago
There's no problem. It's obviously true. Just like the well ordering principle is obviously false. (To explain the joke: they are equivalent, but they strike the intuition very differently.)

122 points by Bogdanp 1y ago

deleted 1y ago

[deleted]

In topology, if you have a continuous surjective map X --> Y, then it might have a continuous splitting (a map the other way which is a "partial" inverse in the sense that Y ---> X ---> Y is the identity) e.g. there are lots of splittings of the projection R^2 ---> R, you could include the line back as the x-axis but also the graph of any continuous function is a splitting. On the other hand, there's no continuous splitting of the map from the unit interval to the circle that glues together the two endpoints. So the category of topological spaces does not have the property "every epimorphism splits." As the article mentions, the axiom of choice says that the category of sets has this property. So we can think of the various independence results of the 20th century as saying, hey, (assuming ZFC is consistent) there's this category, Set, with this rule, and there's this other category called idk Snet, that satisfies the ZF axioms but where there are some surjections that don't split, and that's ok too. Then whatever, if you want to study something like rings but you don't like the axiom of choice, define a rning to be a snet with two binary operations such that blah blah blah, and you've got a nice category Rning and your various theorems about rnings and maybe they don't all have maximal ideals, even though rings do. You're not arguing about ontology or the nature of truth, you're just picking which category to work in.

karmakurtisaani 1y ago
Yeah, it's important to think of these axioms as choosing the rules of the game, rather than what intuitively makes sense. The real question is if playing the game produces useful results.
- btilly 1y ago
  Spoken like a true formalist. It doesn't really have to mean anything when we say that the reals are a larger set than the natural numbers - that's just the conclusion of the game that we are playing. What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with?
  - skissane 1y ago
    > What fraction of people who "know" that there are more reals than natural numbers, do you think really understand that this is not an eternal verity of mathematics, but only a conclusion that follows from a particular set of rules that we're playing the mathematics game with? The claim that there are more reals than naturals holds given classical ZF(C) set theory. But there are alternative set theories in which the reals are countable, e.g. NFU+AxCount. These alternative set theories ensure all reals are countable by rendering Cantor’s diagonalisation argument invalid, since their axioms are too weak to validate it. But, they contain all the same reals as the high school mathematics concept of “reals”. So, there are many reals, and that some of them are countable and others are not are indeed “eternal truths” (it is an eternal truth that whatever axioms have the consequences they do), but the everyday (non-expert) concept of reals isn’t any of them in particular - and it is unclear if the dominance of classical notions in mainstream professional mathematics was historically inevitable or a historical accident - maybe, on the other side of the galaxy, there exists some alien civilisation, in which different foundations of mathematics are mainstream, because their mathematics took a different evolutionary course from ours - maybe for them, reals are classically countable, and uncountability is an exotic notion belonging to alternative foundations of mathematics
    - btilly 1y ago
      As I pointed out at https://news.ycombinator.com/item?id=44271589 https://news.ycombinator.com/item?id=44271589, there are systems that can accept Cantor's argument, without concluding that there are more reals than rational numbers. As you point out, there are many mathematical systems that contain all of the numbers in the high school mathematics concept of "reals". Since those with a high school understanding of reals do not know which of those systems they would agree with, they should not be asked to accept as true, any results that hold in only some of those systems. And that is why I don't like mathematicians telling lay audiences that there are more reals than rationals.
- woopsn 1y ago
  Axioms are also introduced in practical terms just to make proofs and results "better". Usually we talk in terms of what propositions are provable, saying that indicates the strength/power of these assumptions, but beyond this there are issues of proof length and complexity. For example in arithmetic without induction, roughly, theorems remain the same (those which can still be expressed) but may have exponentially longer proofs because of the loss of those `∀n P(n)`-type propositions. In this sense it does sometimes come back to intuition. If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition and doesn't really change "the game" we are trying to play. It just makes it more intuitive and playable.
  - karmakurtisaani 1y ago
    Good point. I would argue, however, that having nicer proofs is a "useful" result of the game.
  - SabrinaJewson 1y ago
    I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545 https://math.stackexchange.com/a/4076545): - ℕ ∪ {∞} - Cardinal arithmetic - ℤ[x]⁺ Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way. I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).
    - deleted 1y ago
      [deleted]
    - woopsn 1y ago
      If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.
alexey-salmin 1y ago
Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.
- gsf_emergency 1y ago
  Careful here, you might wake up the diabol (of pure algebra)
- pfortuny 1y ago
  Yes, but the parent comment is trying to say "imagine the world would only be made up of topological spaces and continuous maps". Then the retraction principle would not hold.
LudwigNagasena 1y ago
How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.
- gylterud 1y ago
  Category theory gives a structural framework for discussing these things. The various categories live side by side and can be related with functors. This allows a broader view and makes it easier perhaps, to understand that there isn’t a right answer to “what is true” about sets in the absolute.
  - LudwigNagasena 1y ago
    But then you would think there is a right answer to “what is true” about categories, and you would face AC again.
    - gylterud 1y ago
      For sure there would have to be a meta theory of some sort. But, I think that many classical mathematicians would be happy with that meta theory to be weaker, rather than stronger. I don't think there is a need for that theory to have AC. After all, thanks to its independence of from the other axioms, AC does not add logical strength to a classical theory. (For die-hard constructivists, such as myself, the story is of course different. But that story is for a another time. I am presenting the classical view here.)

mietek 1y ago

Author of the mechanization here. Feel free to suggest materials from the history of intuitionistic mathematics and type theory that ought to be mechanized and made available to a wider audience — the less well-known, the better.

btilly 1y ago
I wish that I had specific suggestions. My overall wish that more people understood why, in intuitionist mathematics, uncountable means "self-referential" and not "more". No infinite set can have "more" elements than any other, because all things that exist are things that can be written down. And therefore there is a single countable list that includes all things that might possibly have any mathematical existence at all. Anything not on that list does not truly exist. (By internet coincidence, I recently wrote https://math.stackexchange.com/questions/5074503/can-pa-prove-each-goodstein-sequence-can-be-proven-in-pa-to-reach-zero/5075056#5075056 https://math.stackexchange.com/questions/5074503/can-pa-prov... which ends with the beginning of the construction of that list, starting with the Peano axioms. https://news.ycombinator.com/item?id=44269822 https://news.ycombinator.com/item?id=44269822 is about that answer.) Of course Formalists simply write down some axioms, start constructing proofs, and don't worry about what it really means. In what sense do uncountable hordes of real numbers that can never be specified in any way, truly exist? It doesn't matter. These are the axioms that we chose, and that is the statement that we came up with. I have no idea of whether there is a way to formalize or prove the following idea. If there is, it would be good to mechanize it. All notions about uncountable sets being larger than countable ones, require separating the notion of truth from the reasoning required to establish that truth.
- Jtsummers 1y ago
  A nit, but: > Strictly speaking, a programming language doesn't really need comments. "But Lisp has them, and puts them in double quotes." Lisp has comments, but they aren't generally contained in double quotes, you've tossed a lot of strings into your program and called them comments. Comments are either marked with ; (comment to end of line, like //) with conventions on how many semicolons to use in particular places, or comment blocks with #| comment |# (nestable version of /* */). You can add documentation to many definitions, like functions, using strings which may be what you're thinking of but that happens inside the definition like with this: (defun constant (x) "CONSTANT returns a function which always returns X" (lambda (a) x)) Which is a comment, but it's unusual to use strings as comments outside of contexts like that. Also, if you're going to use strings as comments you can make them multi-line instead of doing "I thought about calling these car and cdr..." "...then decided that I'm not really THAT addicted to Lisp" with: "I thought about calling these car and cdr... ...then decided that I'm not really THAT addicted to Lisp" The other reason I'm posting this nit is that if anyone reads your blog/answer and tries to use comments as you've described them inside of expressions they'll be very confused about why it's behaving incorrectly. There's no reason to mislead people, this is not a comment: (if (= 1 2) "Should never be true" ;; that's not a comment, it's an expression (print "Never happens") (print "Always happens")) ;; your interpreter or compiler will complain about this code

jasperry 1y ago

So if I understand the claim of this correctly (I'm a spectator of logic research and haven't tried to follow the proofs), there is a constructive version of AoC that is obviously true, but it's not the same as Zermelo's axiom because that one is extensional. Zermelo's axiom can be formulated in constructive mathematics but gives you things you don't want (like excluded middle.) Is this close to a correct statement of the paper's result? Is all this agreed on today? Have there been any significant refinements?

ncfavier 1y ago
That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from. The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8). Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.
- creata 1y ago
  Off-topic: What's the state of homotopy type theory as an alternative foundation for mathematics? Has it been used to simplify any proofs or prove anything new?
  - zozbot234 1y ago
    Kevin Buzzard (a standard mathematician who has direct expertise in the sorts of things HoTT is supposed to help with) argues that we simply don't know yet. See the references I previously mentioned in https://news.ycombinator.com/item?id=44151283 https://news.ycombinator.com/item?id=44151283

impostervt 1y ago

I've never quite gotten the axiom of choice. Can anyone ELI5?

bobbylarrybobby 1y ago
The Cartesian product of nonempty sets is nonempty. This is obvious!, you might say — obviously we can just pick one element from each set and be done with it. But the statement that we can pick an element from each set is the axiom of choice. Note that it's not necessarily simple to pick an element from a set. For instance, how would one pick an element from the set of uncomputable numbers? A human cannot describe said element, by definition. The axiom of choice says it's possible anyway.
- deleted 1y ago
  [deleted]
- throw310822 1y ago
  Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
  - littlestymaar 1y ago
    As far as I understand there's no such thing “undecidable” in absolute, Gödel incompleteness theorem is about being undecidable under a certain set of axioms.
- moefh 1y ago
  > A human cannot describe said element, by definition. That example doesn't work. Some numbers are describable but not computable, Chaitin's constant being the famous example: https://en.wikipedia.org/wiki/Chaitin%27s_constant https://en.wikipedia.org/wiki/Chaitin%27s_constant
  - deleted 1y ago
    [deleted]

scoofy 1y ago

[flagged]

ptero 1y ago
Axioms should capture the rules we can assume without justification. But in most cases we want them to reflect the rules of the real world in the sense that statements derived from those axioms reflect our observations. That part (reflect observations) can be separated by many levels of abstractions, etc. I would not try visualizing general statements on Lie algebras or spectral theorems, but those abstractions serve the same goal -- help derive conclusions that apply in the real world. My 2c.
- simion314 1y ago
  It is not about real world, choosing an axiom set must simply put produce something valid (with no contradictions) and that is not trivial.
  - dist-epoch 1y ago
    Math is done backwards. We know what kind of results we want to be true, and then we search for the minimum number of axioms which can deliver that.
    - woopsn 1y ago
      There is another goal in addition to minimizing the number/complexity of axioms. Some "axioms" like induction actually introduce an infinite family of assumptions, a so-called schema. So in addition to working backwards from our (incomplete) knowledge, we find certain axioms let us make arguments that are obviously valid but would be formally very tedious without them.
  - ptero 1y ago
    Some math is not about the real world. This is not my kettle of fish, but I have heard of some general topology research directions that discusses properties of topological spaces that probably do not exist at all. Those (according to a friend whose advisor worked in the area) are pretty sad affairs, with only 5-10 people in the world who understand or care about this particular sliver of the math. But some math is about providing tools (again, likely via levels of abstractions) for understanding the world and, to me, this is the "real math". This is a personal view, not an absolute position. I started on the other side of this fence and during my pure math PhD regularly picked fights with our buddies doing physics PhD arguing that mathematics is self-sufficient and does not need any validation from other sciences. But over the next 30 years gradually went to the other side and now think that my original view leads to splintering into gazillion tiny slivers that do not care about anything else; not even about adjacent slivers. Which leads to degeneration. My 2c.

munificent 1y ago

The material is way over my head, but, wow, what a beautifully designed page. The layout and typography is delightful.

deleted 1y ago
[deleted]
mietek 1y ago
Thanks! The source code is set in Fabrizio Schiavi’s amazing PragmataPro. https://fsd.it/shop/fonts/pragmatapro/ https://fsd.it/shop/fonts/pragmatapro/ https://github.com/fabrizioschiavi/pragmatapro https://github.com/fabrizioschiavi/pragmatapro

CliffStoll 1y ago

And the Axiom of Choice implies the Banach-Tarski parodox. It's anti-intuitive: Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun.

dist-epoch 1y ago
The number of pieces is finite, but each piece consists of an infinite number of scattered points: > However, the pieces themselves are not "solids" in the traditional sense, but infinite scatterings of points.
tweakimp 1y ago
Can you really reassemble them into something bigger or just into more copies of the same size?
nwallin 1y ago
> Disassemble a pea into a finite number of pieces. Then reassemble those pieces to create the sun. "Finite number of pieces" is a tricky thing. It's a finite number of pieces, sure, but each of those pieces is made of an uncountably infinite number of pieces. Banach-Tarski is a clever way of sweeping an infinite number of dust bunnies under the rug until just the right moment, when it reveals all infinitely many of them in the shape of a pea and claims to have just created them, when in reality, they were actually there all along, hiding under the rug. For me, Banach-Tarski is just an another version of Hilbert's Hotel, but with uncountable infinities instead of countable ones. Once you accept, in your heart, that infinity is real and is equally deserving of your love and respect as finite natural numbers, then the paradoxicalness of Banach-Tarski melts away.
fpoling 1y ago
Essentially the axiom of choice allows for 3-d sets that do not preserve their volume upon rotation/movement. Such sets, of cause, cannot be constructed or even described as their description will contain infinite number of steps.

revskill 1y ago

[flagged]

jfengel 1y ago

There's no problem. It's obviously true. Just like the well ordering principle is obviously false. (To explain the joke: they are equivalent, but they strike the intuition very differently.)