4 ms·

Somewhat not well known among all mathematical circles, but Diaconescu's theorem states that the law of the excluded middle follows from the axiom of choice[0].

Somewhat not well known among all mathematical circles, but Diaconescu's theorem states that the law of the excluded middle follows from the axiom of choice[0]. This means if you wish to work in constructive mathematics (which has great overlap with computer science), not only you must not take LEM as given but also not take choice as given. There is much to say—mathematically, computationally and philosophically—on the axiom of choice and its variants (countable choice, dependent choice) and subtle interactions with other axioms.[1][2][3] From my experience most mathematicians accept the axiom of choice (or an equivalent statement such as Zorn's lemma[4][5] or Teichmüller-Tukey[6]) because of its pervasiveness and usefulness in many areas of math, such as completeness of first-order logic, existence of a basis of any vector space, showing products of compact topological spaces are compact, and more. [0] Diaconescu's theorem https://en.wikipedia.org/wiki/Diaconescu%27s_theorem https://en.wikipedia.org/wiki/Diaconescu%27s_theorem [1] Exposition of choice, LEM, etc. in Coq http://adam.chlipala.net/cpdt/html/Universes.html http://adam.chlipala.net/cpdt/html/Universes.html [2] Choice vs. countable choice https://mathoverflow.net/questions/22990/choice-vs-countable-choice https://mathoverflow.net/questions/22990/choice-vs-countable... [3] Martin-Löf on choice https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/One-hundred-years-of-Zermelo-s-axiom-of-choice-what-was-the-problem-with-it-2009.pdf https://raw.githubusercontent.com/michaelt/martin-lof/master... [4] Zorn's lemma https://en.wikipedia.org/wiki/Zorn%27s_lemma https://en.wikipedia.org/wiki/Zorn%27s_lemma [5] How to use Zorn's lemma https://gowers.wordpress.com/2008/08/12/how-to-use-zorns-lemma/ https://gowers.wordpress.com/2008/08/12/how-to-use-zorns-lem... [6] Teichmüller–Tukey lemma https://en.wikipedia.org/wiki/Teichm%C3%BCller%E2%80%93Tukey_lemma https://en.wikipedia.org/wiki/Teichm%C3%BCller%E2%80%93Tukey...

veltas 5y ago
Why does AoC implying LEM mean you can't use LEM in constructive maths? EDIT: misread
- siraben 5y ago
  I said that if you don't want to use LEM in constructive maths you must also give up AOC, since AOC -> LEM.
  - veltas 5y ago
    Oh right. Also hi siraben didn't notice it was you.
    - siraben 5y ago
      Hello! Nice to see another IRCer :)
- reuben364 5y ago
  Constructive mathematics by it's nature does not use LEM. The idea is that proof of existance must be done by construction of the object in question. LEM implies DNE, which means existance can be shown by showing non-existance is not the case. EDIT: Apologies, misunderstood.
The_suffocated 5y ago
Is the existence of basis in every vector space really useful? I think in analysis, people mostly work with Schauder basis rather than Hamel basis. I am not aware of any important result that uses the existence of Hamel basis in an infinite-dimensional vector space. This is not a criticism about your comment, but an honest question.
jerf 5y ago
Unsurprisingly, I'm biased in the direction of the Computer Science flavor of mathematics, which leads me to say: Of course the Axiom of Choice is useful. Why wouldn't an axiom that allows you to wave your hand and produce infinite amounts of information that you have no mechanism to produce any of be useful? Of course it's useful to invoke infinite amounts of information from thin air. Indeed, uncountably infinite amounts of information, or any aleph-X you please amounts of information. I agree and understand that it's not a matter of "right" or "wrong", but I do find myself looking a bit askance at "proofs" of statements in which a mathematician writes the equivalent of a few kilobytes of proof statements (in a suitable encoding), which has to be paired with an infinite number of unknowable bits, which the mathematician is not only incapable of providing in practice but often incapable of providing even in theory, to be "true". Mathematicians often claim to find the axiom aesthetic; I find it to be quite the contrary. When you look at proofs from an information-theoretic point of view, the Axiom of Choice is literally an infinitely-sized wart on the side of any proof that uses it.
- lalaithion 5y ago
  This isn't necessarily true; you can also limit which sets are valid sets in a way that guarantees that choosing an element from these sets is well defined. For example, the Axiom of Constructibility basically limits which sets exist, in a way that allows you to always use the Axiom of Choice because your sets have a specific fine grained structure you can use to well-order them. For example, if I were to require "all sets are finite", then the Axiom of Choice is trivial. The Axiom of Constructibility still allows infinite sets (and even uncountable sets), but it's still limited enough that the Axiom of Choice holds. You can almost think of it as requiring all sets to have source code, and then just alphabetizing the source code in order to pick a set.
  - jerf 5y ago
    Yes, it's true that you can use the Axiom of Choice in ways that don't invoke infinite information, and yes, those would be OK with me from an aesthetic point of view. (Again let me emphasize my complaint here is not that it is "invalid" but that I find it very unaesthetic, contra many conventional mathematicians.) But things like the Banach-Tarski paradox definitely require infinite amounts of information (uncountable infinite in this case, I believe) with, as far as I know, no mechanism for producing it. As far as I know, it's just an existence proof. When discussing hypothetical FTL technologies, I often like to say that it's no great surprise that if you allow one impossibility (negative mass) it's no surprise that you get another (FTL). Similarly, if you allow an uncountably infinite amount of information to be magicked into your proof, it's no surprising that you may get a confusing result like the Banach-Tarski paradox. From my perspective, the confusing step isn't when you have two spheres where you used to have one, the confusing step is when you made uncountably-infinitely-precise cuts with no ability to produce the cuts in question. I'm not confused by the end result, I'm confused at that step. So to speak. I'm not literally confused, obviously, only my sense of aesthetics is.
mxwsn 5y ago
I am not a fan of the axiom of choice, and open-minded about truth values beyond true and false. So I'm really curious about the progress of constructive mathematics, regarding proving known results with non-ZNF axioms, and maybe establishing some more "intuitively satisfying" (whatever that may mean) results where ZNF gives subjectively bogus results like Banach-Tarski?
- rwallace 5y ago
  A lot of people blame Banach-Tarski on the axiom of choice. I disagree. I think it's in essence just a variant of the Hilbert hotel, with the axiom of choice merely serving as part of the machinery for this manifestation. In other words, it's just a counterintuitive but true consequence of the nature of infinity. As such, I think any mathematical system that acknowledges infinity, is going to have such counterintuitive results.

veltas 5y ago

Why does AoC implying LEM mean you can't use LEM in constructive maths? EDIT: misread

siraben 5y ago
I said that if you don't want to use LEM in constructive maths you must also give up AOC, since AOC -> LEM.
- veltas 5y ago
  Oh right. Also hi siraben didn't notice it was you.
  - siraben 5y ago
    Hello! Nice to see another IRCer :)
reuben364 5y ago
Constructive mathematics by it's nature does not use LEM. The idea is that proof of existance must be done by construction of the object in question. LEM implies DNE, which means existance can be shown by showing non-existance is not the case. EDIT: Apologies, misunderstood.

The_suffocated 5y ago

Is the existence of basis in every vector space really useful? I think in analysis, people mostly work with Schauder basis rather than Hamel basis. I am not aware of any important result that uses the existence of Hamel basis in an infinite-dimensional vector space. This is not a criticism about your comment, but an honest question.

jerf 5y ago

Unsurprisingly, I'm biased in the direction of the Computer Science flavor of mathematics, which leads me to say: Of course the Axiom of Choice is useful. Why wouldn't an axiom that allows you to wave your hand and produce infinite amounts of information that you have no mechanism to produce any of be useful? Of course it's useful to invoke infinite amounts of information from thin air. Indeed, uncountably infinite amounts of information, or any aleph-X you please amounts of information. I agree and understand that it's not a matter of "right" or "wrong", but I do find myself looking a bit askance at "proofs" of statements in which a mathematician writes the equivalent of a few kilobytes of proof statements (in a suitable encoding), which has to be paired with an infinite number of unknowable bits, which the mathematician is not only incapable of providing in practice but often incapable of providing even in theory, to be "true". Mathematicians often claim to find the axiom aesthetic; I find it to be quite the contrary. When you look at proofs from an information-theoretic point of view, the Axiom of Choice is literally an infinitely-sized wart on the side of any proof that uses it.

lalaithion 5y ago
This isn't necessarily true; you can also limit which sets are valid sets in a way that guarantees that choosing an element from these sets is well defined. For example, the Axiom of Constructibility basically limits which sets exist, in a way that allows you to always use the Axiom of Choice because your sets have a specific fine grained structure you can use to well-order them. For example, if I were to require "all sets are finite", then the Axiom of Choice is trivial. The Axiom of Constructibility still allows infinite sets (and even uncountable sets), but it's still limited enough that the Axiom of Choice holds. You can almost think of it as requiring all sets to have source code, and then just alphabetizing the source code in order to pick a set.
- jerf 5y ago
  Yes, it's true that you can use the Axiom of Choice in ways that don't invoke infinite information, and yes, those would be OK with me from an aesthetic point of view. (Again let me emphasize my complaint here is not that it is "invalid" but that I find it very unaesthetic, contra many conventional mathematicians.) But things like the Banach-Tarski paradox definitely require infinite amounts of information (uncountable infinite in this case, I believe) with, as far as I know, no mechanism for producing it. As far as I know, it's just an existence proof. When discussing hypothetical FTL technologies, I often like to say that it's no great surprise that if you allow one impossibility (negative mass) it's no surprise that you get another (FTL). Similarly, if you allow an uncountably infinite amount of information to be magicked into your proof, it's no surprising that you may get a confusing result like the Banach-Tarski paradox. From my perspective, the confusing step isn't when you have two spheres where you used to have one, the confusing step is when you made uncountably-infinitely-precise cuts with no ability to produce the cuts in question. I'm not confused by the end result, I'm confused at that step. So to speak. I'm not literally confused, obviously, only my sense of aesthetics is.

mxwsn 5y ago

I am not a fan of the axiom of choice, and open-minded about truth values beyond true and false. So I'm really curious about the progress of constructive mathematics, regarding proving known results with non-ZNF axioms, and maybe establishing some more "intuitively satisfying" (whatever that may mean) results where ZNF gives subjectively bogus results like Banach-Tarski?

rwallace 5y ago
A lot of people blame Banach-Tarski on the axiom of choice. I disagree. I think it's in essence just a variant of the Hilbert hotel, with the axiom of choice merely serving as part of the machinery for this manifestation. In other words, it's just a counterintuitive but true consequence of the nature of infinity. As such, I think any mathematical system that acknowledges infinity, is going to have such counterintuitive results.