I’ll just post that as a comment here, since IMO it didn’t really fit in the main body. Since it’s still intended as a sidenote to the original article, it’s really just about how dropping things would affect the original article, and why people would want to.
Quick aside on finitism, constructivism, foundation, choice, etc.
Again, none of this is really relevant if you want to keep everything finite. I’m going to assume you all have a good handle on nice finite things like rational numbers.
Of course, not everyone agrees on just what can be safely assumed when dealing with the infinite. The axiom of choice states that given any collection of sets, no two overlapping each other, there is some set consisting of one element from each. I.e., there is some way to “choose” one element from each, simultaneously. This probably seems obvious—and indeed, if you only have finitely many sets to make choices for, this doesn’t even need to be stated, it’s just a consequence of classical logic that you can pick them one at a time. But allowing it in general has some unintuitive consequences; perhaps more importantly, it’s non-constructive—the axiom assures you there is such a choice, but it can’t in any meaningful way tell you what it is. So constructivists, who insist that any proof that something exists, ought to also tell you what it actually is, will have no truck with it. Weaker forms of it, for those who are uncomfortable with choice but don’t insist on constructivism, include:
The axiom of countable choice—You can make countably many choices simultaneously. This is generally too weak to do much of anything with.
The axiom of dependent choice—A stronger form of countable choice, this allows you to make countably many choices, where each is allowed to depend on the previous ones. This gets used implicitly a lot, but yes, it is in fact a form of choice.
Of course, if you’re such a constructivist that you’re actually a finitist, then I guess you probably accept choice, seeing as it’s true for finite collections of sets! (In classical logic, anyway. I’ll get to that in a moment.)
The axiom of foundation is perhaps also worth noting as somewhat questionable. It just rules out circular (self-containing) or otherwise ill-founded sets. I doubt anyone here particularly wants to admit those, and I don’t know that constructivists have any problem with it; it’s somewhat questionable mostly because it’s essentially never relevant. Ill-founded sets don’t really cause any real pathologies. I only even mention it here because of my mention of Scott’s trick below.
Finally, on logic: Real constructivists actually go a bit further than just pulling out axioms they don’t like; they would insist classical logic itself is too powerful. They reject the principle of the excluded middle, and use a weaker form of logic, intuitionistic logic, which does not include it. So if you ever hear a mathematician say “Well, for that, you have to assume that every sequence of whole numbers is either the constant zero sequence, or includes some nonzero whole number”, relax, they’re not insane, just constructivist.
Note in particular that intuitionistic logic is not strong enough to get you “finite choice” by itself—indeed, if you have finite choice, you get the principle of the excluded middle and the whole thing collapses back to classical logic. So perhaps you could indeed be finitist but still reject choice; in any case, if I’m not mistaken, I think even under intuitionistic logic, finite choice still holds for many sets that will practically come up.
The biggest annoyance of dropping choice (in particular dependent choice) is that conditions that were formerly equivalent stop being so, and you need to make distinctions that were previously irrelevant. This gets much worse if you pass to intuitionistic logic, and start having to specify just what you mean by “real numbers”!
(Then of course there are entirely different set theories out there—I’ve been implicitly assuming ZFC or NBG, but this should only change things for the more set-theoretical sorts of infinities, not the more usual ones.)
I’ll just post that as a comment here, since IMO it didn’t really fit in the main body. Since it’s still intended as a sidenote to the original article, it’s really just about how dropping things would affect the original article, and why people would want to.
Quick aside on finitism, constructivism, foundation, choice, etc.
Again, none of this is really relevant if you want to keep everything finite. I’m going to assume you all have a good handle on nice finite things like rational numbers.
Of course, not everyone agrees on just what can be safely assumed when dealing with the infinite. The axiom of choice states that given any collection of sets, no two overlapping each other, there is some set consisting of one element from each. I.e., there is some way to “choose” one element from each, simultaneously. This probably seems obvious—and indeed, if you only have finitely many sets to make choices for, this doesn’t even need to be stated, it’s just a consequence of classical logic that you can pick them one at a time. But allowing it in general has some unintuitive consequences; perhaps more importantly, it’s non-constructive—the axiom assures you there is such a choice, but it can’t in any meaningful way tell you what it is. So constructivists, who insist that any proof that something exists, ought to also tell you what it actually is, will have no truck with it. Weaker forms of it, for those who are uncomfortable with choice but don’t insist on constructivism, include:
The axiom of countable choice—You can make countably many choices simultaneously. This is generally too weak to do much of anything with.
The axiom of dependent choice—A stronger form of countable choice, this allows you to make countably many choices, where each is allowed to depend on the previous ones. This gets used implicitly a lot, but yes, it is in fact a form of choice.
The Boolean prime ideal theorem or ultrafilter lemma—Not going to explain this here.
Of course, if you’re such a constructivist that you’re actually a finitist, then I guess you probably accept choice, seeing as it’s true for finite collections of sets! (In classical logic, anyway. I’ll get to that in a moment.)
The axiom of foundation is perhaps also worth noting as somewhat questionable. It just rules out circular (self-containing) or otherwise ill-founded sets. I doubt anyone here particularly wants to admit those, and I don’t know that constructivists have any problem with it; it’s somewhat questionable mostly because it’s essentially never relevant. Ill-founded sets don’t really cause any real pathologies. I only even mention it here because of my mention of Scott’s trick below.
Finally, on logic: Real constructivists actually go a bit further than just pulling out axioms they don’t like; they would insist classical logic itself is too powerful. They reject the principle of the excluded middle, and use a weaker form of logic, intuitionistic logic, which does not include it. So if you ever hear a mathematician say “Well, for that, you have to assume that every sequence of whole numbers is either the constant zero sequence, or includes some nonzero whole number”, relax, they’re not insane, just constructivist.
Note in particular that intuitionistic logic is not strong enough to get you “finite choice” by itself—indeed, if you have finite choice, you get the principle of the excluded middle and the whole thing collapses back to classical logic. So perhaps you could indeed be finitist but still reject choice; in any case, if I’m not mistaken, I think even under intuitionistic logic, finite choice still holds for many sets that will practically come up.
The biggest annoyance of dropping choice (in particular dependent choice) is that conditions that were formerly equivalent stop being so, and you need to make distinctions that were previously irrelevant. This gets much worse if you pass to intuitionistic logic, and start having to specify just what you mean by “real numbers”!
(Then of course there are entirely different set theories out there—I’ve been implicitly assuming ZFC or NBG, but this should only change things for the more set-theoretical sorts of infinities, not the more usual ones.)