[HN Gopher] 100 years of Zermelo's axiom of choice: What was the...
___________________________________________________________________
100 years of Zermelo's axiom of choice: What was the problem with
it? (2006)
Author : Bogdanp
Score : 86 points
Date : 2025-06-13 14:46 UTC (8 hours ago)
(HTM) web link (research.mietek.io)
(TXT) w3m dump (research.mietek.io)
| math_comment_21 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| > 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 wrote:
| As I pointed out at
| 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.
| zozbot234 wrote:
| "Cantor's diagonalization argument" is best understood as
| a mere special case of Lawvere's fixed-point theorem.
| Lawvere's theorem is really the meat of the argument, and
| it's also the part that is very easy for exotic systems
| to "accept", since it's close to a purely logical
| argument. Whether these systems truly accept "Cantor's
| argument" is perhaps only a matter of perception and
| intuition, that people may perhaps disagree about.
| btilly wrote:
| It does not matter what your best understanding of
| Cantor's diagonalization argument is. In some
| mathematical systems it means, "there are more reals than
| natural numbers", and in others it means, "the reals
| encode self-reference in a more direct way than the
| natural numbers do".
|
| The result is that it is possible for the acceptance of
| the argument to lead to very different consequences about
| what we then conclude.
| skissane wrote:
| > "Cantor's diagonalization argument" is best understood
| as a mere special case of Lawvere's fixed-point theorem.
| Lawvere's theorem is really the meat of the argument, and
| it's also the part that is very easy for exotic systems
| to "accept", since it's close to a purely logical
| argument.
|
| Okay, but can you prove Lawvere's theorem in NFU+AxCount?
|
| And even if you can, since NFU+AxCount proves that the
| reals are countable, if NFU+AxCount proves Lawvere, then
| (to echo what btilly says in a sibling comment)
| NFU+AxCount+Lawvere couldn't entail the countability of
| the reals, since that would render NFU+AxCount trivially
| inconsistent, and we know it is isn't trivially
| inconsistent (as with any formal system, consistency is
| ultimately unprovable, but if a system is taken seriously
| as an object of mathematical research, then any
| inconsistency must be highly non-trivial.)
| gylterud wrote:
| I agree, but I also want to clarify that cantors argument
| was about subsets of the naturals (N), or more precisely
| functions from N to Bool (the decidable subsets). This is
| where the diagonal argument makes sense.
|
| So to conclude that there are more reals than naturals,
| the classical mathematical argument is:
|
| a) There are more functions N to Bool than naturals.
|
| b) There are as many reals as functions from N to Bool.
|
| Now, we of course agree the mistake is in b) not in a).
| skissane wrote:
| > So to conclude that there are more reals than naturals,
| the classical mathematical argument is:
|
| > a) There are more functions N to Bool than naturals.
|
| > b) There are as many reals as functions from N to Bool.
|
| > Now, we of course agree the mistake is in b) not in a).
|
| Given certain foundations, (a) is false. For example, in
| the Russian constructivist school (as in Andrey Markov
| Jr), functions only exist if they are computable, and
| there are only countably many computable functions from N
| to Bool. More generally, viewing functions as sets, if
| you sufficiently restrict the axiom schema of
| separation/specification, then only countably many sets
| encoding functions N-to-Bool exist, rendering (a) false
| karmakurtisaani wrote:
| > Spoken like a true formalist.
|
| Doesn't seem to be a bad thing. There are some famous
| cranks who reject the concept of infinity, since I suppose
| they have problems wrapping their head around it.
|
| > 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?
|
| People misunderstand mathematics all the time. It's ok,
| it's part of the journey.
| woopsn wrote:
| 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 wrote:
| Good point. I would argue, however, that having nicer
| proofs is a "useful" result of the game.
| SabrinaJewson wrote:
| 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):
|
| - N [?] {[?]}
|
| - Cardinal arithmetic
|
| - Z[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).
| griffzhowl wrote:
| > If for all n we can prove P(n), then `[?]n P(n)` should
| be an acceptable proposition
|
| But how can you prove that P(n) for all n without
| induction? Maybe I misinterpret what you're saying, or I'm
| naive about something in formal languages, but if we can
| prove P(n) for all n. then `[?]n P(n)` just looks like a
| trivial transcription of the conclusion into different
| symbols.
|
| I think the crux of the matter is that we accept inductive
| arguments as valid, and so we formalize it via the
| inductive axiom (of Peano arithmetic). i.e., we accept
| induction as a principle of mathematical reasoning, but we
| can't derive it from something else so we postualte it when
| we come around to doing formalizations. Maybe that's what
| you mean by it coming down to intuition, now that I reread
| it...
|
| Poincare has a nice discussion of induction in "On the
| nature of mathematical reasoning", reprinted in Benacerraf
| & Putnam Philosophy of Mathematics, where he explicates it
| as an infinite sequence of modus ponens steps, but
| irreducible to any more basic logical rule like the
| principle of (non-)contradiction
| zozbot234 wrote:
| Rejecting induction could be quite useful if you want to
| be very precise about the implications of your
| constructions wrt. computational complexity. This is of
| course only a mildly strengthened variant of the usual
| arguments for constructivism.
| alexey-salmin wrote:
| Doesn't "continuous" make all the difference here? AC doesn't
| contain a comparable limitation, so the analogy doesn't work
| that week.
| LudwigNagasena wrote:
| How is it different from using ZF as a meta-theory to study
| ZF(C)? Is there anything special about category theory vis-a-
| 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 wrote:
| 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.
| mietek wrote:
| 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 wrote:
| 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-prov...
| which ends with the beginning of the construction of that list,
| starting with the Peano axioms.
| 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 wrote:
| 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
| btilly wrote:
| Thank you, fixed.
|
| And that is why I did think that. I only play with the
| ideas of Lisp. I've never really had to use it. So I looked
| at a Lisp example, saw something that looked like it was
| functioning as a comment, then used that comment style.
| SabrinaJewson wrote:
| Relevant to this is Skolem's paradox
| (https://en.wikipedia.org/wiki/Skolem%27s_paradox), which
| states that any uncountable set can be modelled by a
| countable set.
|
| In that light, the statement that the reals have greater
| cardinality than the naturals can be thought of as a
| statement that _our model of set theory_ happens to contain
| no injections from the reals to the naturals. Not that they
| can't exist in a Platonic sense, or even just in the
| metatheory.
| btilly wrote:
| That does seem extremely relevant. And is a mirror of the
| fundamental insight behind nonstandard analysis. Which is
| that that any set containing the integers that follows some
| set of axioms, has a nonstandard model that follows a
| nonstandard version of those axioms, and which contains
| infinite integers.
|
| This can be seen as why it is different for a set of axioms
| to prove that it proves something, than it is to prove
| something directly. Because when the axioms prove that they
| prove, you might be in a nonstandard model where that
| "proof" is infinitely long, and therefore isn't really a
| proof!
|
| And that is why, for example, if PA is consistent, then it
| remains consistent if you extend PA with the axiom, "PA is
| not consistent". Clearly any model of that extended set of
| axioms does not describe what we want PA to mean. But that
| doesn't mean that it logically contradicts itself, either.
| woolion wrote:
| From the point of view of proof-theory, you can show that PA
| (arithmetic) is equivalent to the consistency of the omega
| cardinal (the countable infinite). Basically, everything line
| up quite well between things you want to be true and things
| that are true in that system. This equivalence breaks down
| with higher-order system such as System F, but it gives a
| system that may feel more natural, especially to programmers.
| The problem that explains the endurance of "formalism" is
| that there are so many things that you "want to be true" that
| can't be shown to be true in intuitionistic systems is a real
| issue. For instance, simply proving that a fast-growing
| function is total. You are fine with recurrence, but not if
| the function grows too fast? This sounds really stupid. But I
| don't think many people care that much, they'll just use
| whatever give them results.
| btilly wrote:
| It is certainly easier to prove interesting theorems with
| formalism. You don't get caught up with such basic things
| like whether or not it is always possible to tell that one
| real number is bigger than another.
|
| But formalism leads to having to accept conclusions that
| some of us don't like. I already referred to the existence
| of uncountably many things that cannot in any useful way
| ever be specified. If you include the axiom of choice, you
| get the Banach-Tarski paradox. Mathematicians debated that
| one for a while, but now generally accept it.
|
| My favorite example of a weird conclusion comes from https:
| //en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theo....
| We can non-constructively prove the following facts. Any
| class of graphs that is closed under the graph minor
| operation (for example planar graphs), has a finite set of
| forbidden graph minors that completely characterize the
| graph (in the case of planar graphs, K5 and K3,3). In
| general, there is no way to find those forbidden graph
| minors. Even if you were given the complete list, you
| couldn't necessarily verify that the list was correct. You
| cannot necessarily even find an upper bound on how big this
| set is.
|
| By "cannot necessarily" I mean, "it is sometimes
| unprovable".
|
| In what sense can a finite set exist and be finite when it
| is unfindable, unverifiable, and has unboundable size?
|
| To make this concrete, there are 17,523 known forbidden
| minors for the toroidal graphs. We don't know how to find
| more. We don't know if we have the full list. And we don't
| have an upper bound on how many more of them there are to
| be found.
|
| You're free to accept this ephemeral claim to existence as
| actual existence. But this existence isn't very useful for
| us.
| woolion wrote:
| I'm fine with that. I don't think it's much worse than
| the quirks of what you call non-formalists systems.
|
| In your original comment, you mention:
|
| All notions about uncountable sets being larger than
| countable ones, require separating the notion of truth
| from the reasoning required to establish that truth.
|
| If you wanted to formalize something like that, you'd
| need the consistency of an absurdly large cardinal. I
| think it is an interesting type of question to explore,
| so it's fine to have these large cardinals.
| btilly wrote:
| I believe that you're fine with it, simply because that
| is what you're familiar with. And if you'd grown up with
| a different way of thinking about these problems, then
| you wouldn't be fine with it.
|
| Personally, I can work with either system. But, to me,
| formalism really does feel like a game. And the more that
| I have thought about the foundations of math, the more
| dissatisfied I have become with this game. And now I find
| myself frustrated when people assert the conclusions of
| the game as truth, instead of as merely being formal
| statements within a game that mathematicians are choosing
| to play.
|
| Here is something that I believe.
|
| We owe our current understanding of uncountability to
| Cantor's metaphor, about figuring out which group of
| sheep is larger by pairing them off. We would today have
| a very different kind of mathematics if Cantor had
| instead made a more careful analogy to the problem of
| trying to count all of the sheep that have ever existed.
| Even if you had perfect information about the past,
| you're doomed to fail because you can't figure out where
| to draw the line between ancestral sheep, and sheep-like
| ancestors.
|
| This second metaphor is exactly parallel to
| uncountability within the computable universe. For
| example we can implement reals as some kind of Cauchy
| sequences. For example as programs for functions f, where
| f(n) is a rational, and |f(n) - f(m)| <= 1/n + 1/m. This
| works perfectly well. But now Cantor's diagonalization
| argument clearly does not demonstrate that there are more
| reals. Instead it demonstrates the limits of what
| computation can predict about the behavior of other
| computations.
|
| In other words, I just described a system operating on a
| notion of truth that is directly tied to the reasoning
| required to establish that truth. And in that system,
| uncountable is tied to self-reference. And really doesn't
| mean more.
|
| I don't know how to really formalize this idea. But I'd
| be interested if anyone actually has done so.
| pron wrote:
| > In what sense can a finite set exist and be finite when
| it is unfindable, unverifiable, and has unboundable size?
|
| In the same sense that we could say that every computer
| program must either eventually terminate or never
| terminate without most people thinking there's a major
| philosophical problem here.
|
| And by the way, the very same question can be (and has
| been) levelled at constructivism: in what sense does a
| result that would take longer than the lifetime of the
| universe to compute exist, as it is unfindable and
| unverifiable?
|
| Look, I think that it is interesting to work with
| constructive axioms, but I don't think that humans
| _philosophically_ reject non-constructive results. It 's
| one thing to say that we can learn interesting things in
| constructive mathematics and another to say there's a
| fundamental problem with non-constructive mathematics.
|
| > But formalism leads to having to accept conclusions
| that some of us don't like.
|
| At least in Hilbert's sense, I don't think formalism says
| quite what you claim it says. He says that _some_
| mathematical statements or results apply to things we can
| see in the world and could be assigned meaning through,
| say, correspondence to physics. But other mathematical
| statements don 't say anything about the physical world,
| and therefore the question of their "actual meaning" is
| not reason to reject them as long as they don't lead to
| "real" results (in the first class of statements) that
| contradict physical reality.
|
| Formalism, therefore, doesn't require you to accept or
| reject any particular meaning that the second class of
| statements may or may not have. If a statement in the
| second class says that some set exists, you don't _have_
| to assign that "existence" any meaning beyond the
| formula itself.
| btilly wrote:
| My understanding of how Hilbert meant it is summed up in
| this quote from him: _" Mathematics is a game played
| according to certain simple rules with meaningless marks
| on paper."_ I think that in part because I read Constance
| Reid's excellent biography _Hilbert!_ It traces in some
| detail his thinking over his life, and how he came to
| formalism. His thinking about the nature of existence was
| particularly interesting.
|
| If you think that he meant something else, please find
| somewhere where he said something that didn't boil down
| to that.
|
| As for what most people think about the philosophical
| implications, nobody should be expected to have any
| meaningful philosophical opinions about topics that they
| have not yet tried to think about. I know that I didn't.
|
| After you've thought about it, you may well have a
| dramatically different opinion than I do. For example
| Godel thought that mathematical existence was real, since
| mathematics exists in God's mind. This idea made it
| important to him to decide which set of axioms was right,
| where right means, "These are the axioms that God must
| have settled on, and that therefore exist in His mind."
| This lead to such ironies as the fact that after proving
| that the consistency of ZF implies the consistency of
| ZFC, he then concluded that that the construction was so
| unnatural that Choice couldn't be one of God's axioms!
|
| I don't agree with Godel. For a start, I don't believe
| that God exists. And after I thought about it more, I
| realized that what I want existence to mean, isn't what
| mathematicians mean when they say "exists". I'm willing
| to use language in their way when I'm talking to them.
| But I'm always aware that it doesn't mean what I want it
| to mean.
| pron wrote:
| I can't locate my Heijenoort right now, but here's a
| description from the Stanford Encyclopedia of Philosophy
| [1] (which points to Heijenoort):
|
| _The analogy with physics is striking... In the second
| half of the 1920s, Hilbert replaced the consistency
| program with a conservativity program: Formalized
| mathematics was to be considered by analogy with
| theoretical physics. The ultimate justification for the
| theoretical part lies in its conservativity over "real"
| mathematics: whenever theoretical, "ideal" mathematics
| proves a "real" proposition, that proposition is also
| intuitively true. This justifies the use of transfinite
| mathematics: it is not only internally consistent, but it
| proves only true intuitive propositions (and indeed all,
| since a formalization of intuitive mathematics is part of
| the formalization of all mathematics)._
|
| _In 1926, Hilbert introduced a distinction between real
| and ideal formulas. This distinction was not present in
| 1922b and only hinted at in 1923. In the latter, Hilbert
| presents first a formal system of quantifier-free number
| theory about which he says that "The provable formulae we
| acquire in this way all have the character of the
| finite"_
|
| In other words, Hilbert does not require assigning any
| sense of truth _beyond the symbolic one_ to those
| mathematical statements _that do not_ correspond to
| physical reality, but those statements that can
| correspond to physical reality (i.e. the "real
| formulas") must do so, and those "real formulas" are
| meaningfully true beyond the symbols.
|
| The earlier formalism (mathematics is just symbols) could
| no longer be justified after Godel, as consistency was
| its main justification.
|
| If anything, I think it's constructivism that suffers
| from a philosophical issue in requiring meaning that
| isn't physically realisable -- unlike ultrafinitism, for
| example. Personally, I find both Hilbert's formalism and
| ultrafinitism more philosophically satisfying than
| constructivism, as they're both rooted in physical
| reality, whereas constructivism is based on "computation
| _in principle_ " (but not in practice!).
|
| > As for what most people think about the philosophical
| implications, nobody should be expected to have any
| meaningful philosophical opinions about topics that they
| have not yet tried to think about
|
| I mean people who have thought about it.
|
| [1]: https://plato.stanford.edu/entries/hilbert-program/
| btilly wrote:
| I was responding to this statement of yours, _" I don't
| think that humans philosophically reject non-constructive
| results."_
|
| Some of the humans who have thought about it do reject
| them. Some of the humans who have thought about it don't
| reject them.
|
| Most humans, including most mathematicians, have never
| truly thought about it.
| pron wrote:
| > Some of the humans who have thought about it do reject
| them.
|
| I think they reject them only if they misrepresent
| Hilbert's formalism, because formalism does not assign
| them _any_ meaning of truth beyond the symbolic. It makes
| no statement that could be rejected: a mathematical
| theorem that proves a set "exists" does not necessarily
| make any claim about its "actual" existence (unlike, say,
| Platonism). You asked in what sense does such a set
| exist, and Hilbert would say, great question, which is
| why I don't claim there necessarily is _any_ such sense.
|
| What those who reject Hilbert's formalism reject is the
| validity of a system of mathematics where only some but
| not all propositions are "externally" meaningful, but
| such a rejection, I think, can only be on aesthetic
| grounds, because, again, for Hilbert, all "valid"
| foundations must agree with physical reality when it
| comes to statements that could be assigned physical
| meaning. If ZFC led to any result that doesn't agree with
| physical reality, Hilbert would reject it, too. But it
| hasn't yet.
| btilly wrote:
| I believe that you are misrepresenting Hilbert here.
|
| If ZFC led to a result that doesn't agree with physical
| reality, Hilbert would not reject that result. Instead,
| at worst, he would simply move it from the category of
| being a real formula, to being an ideal formula. For
| example, Euclid's geometry doesn't agree with physical
| reality. Therefore it is an ideal formula, not a real
| formula. And yet we do not reject this geometry from
| mathematics.
|
| But the distinction between real and ideal is a question
| for physics. It is not a question that mathematicians
| need worry about. The questions that mathematicians need
| worry about are entirely those which are internal to the
| formal game.
| zozbot234 wrote:
| > Look, I think that it is interesting to work with
| constructive axioms, but I don't think that humans
| philosophically reject non-constructive results.
|
| I don't think the point of constructivism is to
| "philosophically reject non-constructive results". You
| can accept non-constructive results just fine as a
| constructivist, so long as they're consistently rephrased
| as negative statements, i.e. logical statements starting
| with "NOT ...". This is handy in some ways (you now know
| instantly what statements correspond to "direct" proofs
| that can be given a computational semantics and even be
| reused for all sorts of computer sciencey stuff) and not
| so handy in others (to some extent, it comes with a kind
| of denial about the inherently "dual" nature of the
| fragment of your constructive logic that contains all
| that negatively-phrased stuff). But these are matters of
| aesthetics and perceived elegance, more than philosophy.
|
| The duality concern is one that some will want to address
| by moving even further to linear logics (since these are
| "dual" like classical logic but also allow for
| constructive statements) but of course that's yet another
| can of worms in its own right.
| btilly wrote:
| When you talk about the point of constructivism, do you
| mean currently, or historically?
|
| For me, personally, the point of constructivism is to
| wind up talking about mathematics in a language that
| corresponds with what I want words to mean. I personally
| want mathematical existence to mean something that could
| be represented in an ideal computer. And existence in
| classical mathematics means something very different than
| that.
|
| But historically, the point of constructivism was to try
| to avoid paradoxes through careful reasoning. At least
| that is my understanding. You're welcome to read http://t
| hatmarcusfamily.org/philosophy/Course_Websites/Readi...
| and decide if that is what Brouwer meant.
|
| Unfortunately for this historical motivation, Godel
| proved that every classical mathematical proof can be
| mechanically transformed into a purely constructive
| proof, possibly of a much more carefully worded
| statement. With the result that if there is a
| contradiction within classical mathematics, there is also
| a contradiction within constructivism.
|
| Luckily it has been so long since our foundations of
| mathematics fell apart because of someone finding a
| contradiction, that we no longer worry about it. (Was the
| set of all sets that do not contain themselves the last
| such contradiction? I think it might have been.)
| zozbot234 wrote:
| You could argue that the early constructivists' notions
| of "paradoxes" included things such as "statements about
| the existence of things that we don't know how to
| explicitly construct, and that may be even impossible to
| explicitly construct in the general case". Under Godel's
| argument, these statements (like other classical
| statements) become mere _negative_ statements asserting
| the non-existence of anything that might contradict the
| aforementioned non-constructive objects. So, they 're no
| longer "paradoxical" in that sense. Stated another way,
| decidability/computability (perhaps relative to some
| appropriate oracle, to fully account for the surprising
| strength of some loosely-"constructive" principles) is
| not quite the same concern as consistency. Of course,
| this was all stated in very fuzzy and imprecise terms to
| begin with (no real notion back then of what "decidable"
| and "computable" might mean), so there's that.
| IsTom wrote:
| > In what sense can a finite set exist and be finite when
| it is unfindable, unverifiable, and has unboundable size?
|
| The way I see it is that an existence of proof isn't
| required for something to be true. Something being true
| is a matter of the model, being provable is a matter of
| axioms and deduction rules. And there comes the
| distinction between [?] and [?].
| layer8 wrote:
| > 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.
|
| The universe (in the cosmological sense) can be written down
| as a single countable list, and anything different would be
| impossible? Or are you saying that it does not truly exist?
| I'm not sure how that makes sense.
| btilly wrote:
| We can create a countable list that contains every possible
| description that can ever be created. For example just
| write down numbers in base ASCII, using a programmable
| markup language (like TeX) that lets us represent anything
| that we want. (OK, TeX can only describe shapes down to the
| wavelength of visible light, but that's good enough for
| me.)
|
| In what sense does an idea exist when it cannot be
| described by anything on that list?
| layer8 wrote:
| To quote an old adage, the map isn't the territory. That
| we can't fully write it down (which we can't even for
| countable infinities, or even something like 10^10^10
| symbols) doesn't mean that it doesn't exist. All of the
| territory still exists, even if any map that we can draw
| will only capture certain aspects of it.
|
| Regarding "ideas", to me math is primarily exploration
| and discovery, rather than invention. That's one way how
| it corresponds to the territory analogy.
| cvoss wrote:
| > there is a single countable list that includes all things
| that might possibly have any mathematical existence at all.
|
| Help me understand that. Isn't the Cantor diagonialization
| argument a proof that such a list cannot exist because,
| supposing it did exist, it could be used to construct an
| object not on the list? Are you proposing that your list
| somehow defeats Cantor here?
|
| (Of course, we're using the word "list" loosely here. What we
| mean is a total function with domain Nat, right?)
| btilly wrote:
| Please see my comment at
| https://news.ycombinator.com/item?id=44271589 for my
| explanation.
| franklin_p_dyer wrote:
| Really cool post! This is an awesome idea and I'd love to see
| more of these. :-)
|
| Maybe these won't be the kind of thing you are looking for, but
| here are some gems that would be cool to see formalized, some
| of which I've been meaning to do myself someday:
|
| - There are many parts of the book "A Course in Constructive
| Algebra" (Mines, Richman, Ruitenburg) worthy of being
| formalized, but even just the discussion of "omniscience
| principles" in the first chapter would be cool.
|
| - I absolutely love Sierpinski's book "Cardinal and Ordinal
| Numbers", and although I'm not sure it would be considered a
| book of "intuitionistic mathematics", he is careful enough
| about pointing out where he uses AoC for parts of his book to
| be suitable for consideration. The results and exercises in
| VI.5 "Axiom of choice for finite sets" are probably my favorite
| in the whole book and would be awesome to see formalized.
|
| - Tarski's Theorem about Choice: https://en.wikipedia.org/wiki/
| Tarski%27s_theorem_about_choic..., particularly from Tarski's
| original paper (though it is in French).
|
| - I am not sure about a historical article/source for this one,
| but formalization of some results about Dedekind-finite and
| Dedekind-infinite sets (https://en.wikipedia.org/wiki/Dedekind-
| infinite_set) could be really fun. I find these to be very
| counterintuitive.
| gylterud wrote:
| I would suggest Bishop's Constructive Analysis.
|
| And a plug: I have a formalisation of models of constructive
| set theory in Homotopy Type Theory here:
| https://git.app.uib.no/hott/hott-set-theory
| jasperry wrote:
| 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 wrote:
| That sounds about correct. The naive interpretation of AC that
| interprets [?] as S and [?] as P amounts to the trivial fact
| that P distributes over S, which has little to do with any
| choice principle. If you instead interpret it in setoids, as
| Martin-Lof 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_ S-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 wrote:
| 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 wrote:
| 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
| impostervt wrote:
| I've never quite gotten the axiom of choice. Can anyone ELI5?
| bobbylarrybobby wrote:
| 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.
| throw310822 wrote:
| Isn't that equivalent (or, ok, similar) to saying that we can
| decide undecidable mathematical truths?
| littlestymaar wrote:
| As far as I understand there's no such thing "undecidable"
| in absolute, Godel incompleteness theorem is about being
| undecidable under a certain set of axioms.
| moefh wrote:
| > 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
| SabrinaJewson wrote:
| > 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.
|
| No? I don't see how this relates to AC at all. AC is about
| making an infinite number of choices at once - if you're just
| making two choices (or, more generally any finite number of
| choices), as is needed here to prove that this Cartesian
| product is nonempty, then that's completely fine without
| extra axioms. See for example
| https://mathoverflow.net/q/32538
|
| E.g. in type theory, one term of type `Nonempty(A) -
| Nonempty(B) - Nonempty(A x B)` (supposing that `Nonempty` is
| defined as the [bracket
| type](https://ncatlab.org/nlab/show/bracket+type)) would just
| be `l [a] - l [b] - [(a, b)]`.
| gjm11 wrote:
| What AC's equivalent to is "the Cartesian product of _any
| set of nonempty sets_ is nonempty ". Not just of _two_
| nonempty sets, for which indeed you don 't need AC.
| Kranar wrote:
| The two statements imply each other, they are logically
| equivalent:
|
| https://en.wikipedia.org/wiki/Product_topology#Axiom_of_cho
| i...
|
| >One of many ways to express the axiom of choice is to say
| that it is equivalent to the statement that the Cartesian
| product of a collection of non-empty sets is non-empty.
| moomin wrote:
| This seems elegant, but you need that you can take a
| Cartesian product and turn it into a set of its elements as
| well. I don't know if that's provable without classic AoC.
| (It might be.)
| drdec wrote:
| > The Cartesian product of nonempty sets is nonempty.
|
| I think you want: the Cartesian product of an infinite number
| of (potentially infinite) non-empty sets is non-empty.
| a_cardboard_box wrote:
| > 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?
|
| In ZF without choice, you can pick an element from any non-
| empty set, so it actually is simple to pick _an_ element from
| _a_ set. Choice is only needed when you have an infinite
| number of sets to pick elements from.
| WhitneyLand wrote:
| Yes. Here's a great ELI5 intro:
|
| https://youtu.be/_cr46G2K5Fo?si=Q6iEm3m-Nyge3FUW
| dandanua wrote:
| Have you ever seen statements such as "for every epsilon there
| is a delta such that the following ... holds"? The axiom of
| choice implies that in those cases the delta can be supplied by
| some function of epsilon. It can't be proven that such a
| function exists in ordinary ZF (even if you can prove that
| statement with epsilon and delta).
| moomin wrote:
| If you have a set of sets, you can pick one element from each
| set to construct another set.
|
| This is provable if everything's finite, but not if you're
| dealing with things with bigger cardinalities like the real
| numbers.
| nobodyandproud wrote:
| Not like 5, but High-school Geometry.
|
| If you remember Geometry, there are two ways to prove
| something:
|
| - By making it (constructing)
|
| - By contradiction (reductio ad absurdum)
|
| During the late 1800s to early 1900s, when math was becoming
| more formalized, a group of mathematicians had issues with the
| second method.
|
| From their point of view if you can't show how to make it, then
| you've not proven that it exists.
|
| Now it turns out that indirect proofs like contradiction
| requires the law of excluded middle: If something isn't true,
| then it must be false (or vice versa).
|
| It turns out that AoC is needed/implied, for the law of
| excluded middle; hence the objection to AoC; and enables these
| non-constructive proofs.
|
| https://en.m.wikipedia.org/wiki/Law_of_excluded_middle
|
| Another AoC proof: Prove that an irrational number to a
| irrational power can be rational.
|
| sqrt(2)^sqrt(2) : If rational, then done.
|
| Else (sqrt(2)^sqrt(2))^sqrt(2) = 2.
|
| QED (and non-constructive).
| ncfavier wrote:
| Note that this proof doesn't require the axiom of choice,
| only excluded middle.
| Sniffnoy wrote:
| AC is _much_ stronger than excluded middle. This doesn 't
| really say anything about what AC does.
| IngoBlechschmid wrote:
| This set of slides, originally devised for the Chaos
| Communication Congress, might be helpful:
| https://www.speicherleck.de/iblech/stuff/ac-38c3.pdf
|
| - Precise statement of the axiom
|
| - Overview of its consequences
|
| - A counterexample (in an alternative universe)
|
| - Consistency of the axiom
|
| - Godel's sandbox for containing the axiom
| Sniffnoy wrote:
| The axiom of choice allows you to make infinitely many
| arbitrary choices.
|
| You don't need the axiom of choice to make finitely many
| arbitrary choices. Let's say you have a pile of
| indistinguishable socks in front of you. You want to pick two
| of them. Well -- assuming that there are at least two of them
| to pick -- you can pick one, and then you can pick one from
| what remains. If something exists, you can pick one of it,
| that's permitted by the laws of logic; and if you need to do
| that multiple times, well, obviously you can just do it
| multiple times. But if you need to do it _infinitely_ many
| times, well, the laws of logic aren 't enough to support that.
|
| You also don't need the axiom of choice if the choices aren't
| arbitrary, but rather are given by some rule you can specify.
| There's a famous analogy used by Russell to illustrate this.
| Suppose you have set in front of you an infinite array of pairs
| of socks, and you want to pick one sock from each pair. Then
| you need the axiom of choice to do that. But suppose, instead,
| it were an infinite array of pairs of _shoes_. Then you don 't
| need the axiom of choice! Because you can say, I will always
| pick the left one. That's a _rule_ according to which the
| choice is made, so you don 't need the axiom of choice. You
| only need the axiom of choice when the choices have some
| arbitrary element to them, where there isn't a rule you can
| specify that gets things down to just a single possibility.
| (Isn't the choice of left over right making an arbitrary
| choice? In a sense, yeah, but it's only making a _single_
| arbitrary choice!)
|
| (The axiom that lets you do this, btw, is the axiom of
| separation. Or, perhaps in rare instances, the axiom of
| replacement, but the axiom of replacement is generally
| irrelevant in normal mathematics.)
|
| So that's what the axiom of choice does. Without it, you can
| only make finitely many arbitrary choices, or infinitely many
| specified choices. If you need to make infinitely many choices,
| but you don't have a rule to do it by, you need axiom of
| choice.
|
| [Edit: Given the article, I should note that I'm describing the
| role of the axiom of choice in ordinary mathematics, rather
| than its role in constructive mathematics. I know little about
| the latter.]
| krick wrote:
| Somehow the existing answers don't satisfy me, so here's my
| attempt. The essence of it is really simple.
|
| The axiom is an obviously true statement: if you have a bag of
| beans, you can _somehow_ take one bean out of it, without
| specifying, how do you choose the exact bean. Obvious, right?
| And that 's really it, informally this is the axiom of choice:
| we are stating that we can _somehow_ always do that, even if
| there are infinitely many beans and infinitely many bags, and
| the result of your work may be a collection of infinitely many
| beans.
|
| Now, what's the "problem"? If you look closer, what I've just
| said is equivalent to saying we can well-order[0] any set of
| elements, which must make you uncomfortable: you may be ok with
| the idea that in principle you can order infinitely many
| particles of sand (after all, there are just N of them), but
| how the fuck do you order _water_ (assuming it 's like R --
| there are no molecules and you can divide every drop infinitely
| many times)?
|
| This is both why we have it -- R seems like a useful concept so
| far; and the source of all notorious "paradoxes" related to it
| -- if you can somehow order water, you may as well be able to
| reorder details of a sphere in a way to construct 2 spheres of
| the same size.
|
| [0] https://en.wikipedia.org/wiki/Well-ordering_theorem
| scoofy wrote:
| Axioms are arbitrary. Use them if they are useful.
| ptero wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| The material is way over my head, but, wow, what a beautifully
| designed page. The layout and typography is delightful.
| CliffStoll wrote:
| 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 wrote:
| 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 wrote:
| Can you really reassemble them into something bigger or just
| into more copies of the same size?
| jfengel wrote:
| 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.)
___________________________________________________________________
(page generated 2025-06-13 23:00 UTC)