[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 : 114 points
Date : 2025-06-13 14:46 UTC (1 days 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
| IngoBlechschmid wrote:
| Indeed, what you write is true from an external point of
| view; just note that _within_ this flavor of constructive
| mathematics, the set of functions from N to Bool is
| uncountable again.
|
| There is no paradox: Externally, there is an enumeration
| of all computable functions N -> Bool, but no such
| enumeration is computable.
| skissane wrote:
| Is it internally uncountable in the strong sense that the
| system can actually prove the theorem "this set is
| uncountable", or only in the weaker sense that it can't
| prove the theorem "this set is countable", but can't
| prove its negation either?
|
| If the latter, what happens if you add to it the
| (admittedly non-constructive) axiom that the set in
| question is countable?
| btilly wrote:
| It should be true in the stronger sense.
|
| Suppose that you've written down a function enumerate,
| that maps all natural numbers to functions that
| themselves map all natural numbers to booleans. We then
| can write down the following program.
| (defn unenumerated (n) (not ((enumerate n) n)))
|
| This function can be recognized as Cantor
| diagonalization, written out as a program.
|
| If enumerate actually works as advertised, then it can't
| ever find unenumerated. Because if (enumerate N) is
| unenumerated, then ((enumerate N) N) will hit infinite
| recursion and therefore doesn't return a boolean.
|
| This argument is, of course, just Cantor's
| diagonalization argument. From an enumeration, it
| produces something that can't be in that enumeration.
| skissane wrote:
| > If enumerate actually works as advertised, then it
| can't ever find unenumerated. Because if (enumerate N) is
| unenumerated, then ((enumerate N) N) will hit infinite
| recursion and therefore doesn't return a boolean.
|
| Okay, but if we take the position that only non-halting
| (for all inputs) programs represent functions over N, if
| your program "unenumerated" never halts for some N, it
| doesn't represent a function, so your argument isn't a
| case of "using the enumeration of all functions to
| produce something which doesn't belong to the
| enumeration"
|
| Obviously an enumeration of all computable functions
| isn't itself computable. But if we consider Axiom
| CompFunc "if a function over N is computable then it
| exists" (so this axiom guarantees the existence of all
| computable functions, but is silent on whether any non-
| computable functions exist) and then we consider the
| additional Axiom CountReals "there exists a function from
| N to all functions over N", then are those two axioms
| mutually inconsistent? I don't think your argument, as
| given, directly addresses this question
| btilly wrote:
| It's just a straight up liar's paradox. If enumerate is a
| function that works as advertised, then unenumerated is
| as well. If enumerate tries to list unenumerated, then
| enumerate can't work as advertised.
|
| For the argument that I gave to work, you need what you
| might call Axiom ComposeFunc, you may always compose a
| new function by taking an existing function and doing
| something that is known to be valid with it. Obviously
| this axiom is true about the computable universe. But,
| more than that, it is also true about any generalization
| of "function" that behaves like most would expect a
| function to have.
|
| Now it is true that your Axiom CompFunc and Axiom
| CountReals do not necessarily contradict each other. But
| CompFunc, ComposeFunc and CountReals do contradict each
| other, and the contradiction can be built by following
| Cantor's diagonalization argument.
| skissane wrote:
| > But, more than that, it is also true about any
| generalization of "function" that behaves like most would
| expect a function to have.
|
| It isn't true in NFU though, correct? At least not in the
| general case. Because Cantor's argument fails in NFU
| btilly wrote:
| If I understand what I just Googled correctly (definitely
| not guaranteed), the reason why Cantor's argument can
| fail in NFU is that NFU does not necessarily allow you to
| build a function that returns things in X, out of a
| function that returns functions returning things in X.
|
| So it has non-computable functions, but also has a type
| system that tries to avoid allowing self-reference. And
| that type system gets in the way of Cantor's argument.
|
| I clearly hadn't thought of this possibility. It is a
| constraint of a kind that doesn't show up in the
| computable universe.
|
| And so, going back, if the the Russian constructivist
| school does indeed center on computability, then my first
| answer to you was correct.
| skissane wrote:
| Right, I think we are in agreement - a pure Russian
| constructivist approach which only permits computable
| functions cannot prove the reals are countable. However,
| I still am sceptical it can prove they are uncountable-if
| you limit yourself to computable constructions, you can't
| actually computably construct a Cantor diagonal, so his
| argument fails just like it does in NFU.
|
| The (un)countability of the reals is known to be
| independent of NFU-it is consistent both with the reals
| being countable and them being uncountable. There are two
| different axioms which it is standard to add to NFU to
| decide this-AxCount<= which implies the reals are
| countable and AxCount>= which implies the reals are
| uncountable.
|
| I guess I was suggesting that in the same way, an
| additional axiom could be added to computable set theory
| which renders the reals countable or uncountable. If an
| additional axiom asserting the countability of the reals
| involves the existence of a function from the naturals to
| functions over the naturals, that would obviously be
| introducing an uncomputable function-but for that to
| produce an inconsistency, it would need to enable
| Cantor's argument-and, given your "ComposeFunc" in the
| computable universe is already restricted to only
| operating over computable functions, it is reasonable to
| limit its application to computable functions in an
| extension, which would mean the addition of this
| uncomputable function would still not permit Cantor's
| argument
| gylterud wrote:
| There is nothing uncomputable with the cantor
| diagonalisation. The Russians gladly accept it, I assure
| you. Here is a Haskell implementation:
|
| diag :: (nat -> (nat -> Bool)) -> (nat -> Bool)
|
| diag f n = not (f n n)
|
| The following argument is also constructive. Just like in
| classical mathematics, crustructive mathematics proves
| the negation of A by assuming A and deriving a
| contradiction. (But you cannot prove A by assuming it's
| negation and deriving a contraction):
|
| Assume a surjectiom f :: nat -> Bool. Then there is x
| such that f x = diag f. Since these two functions are
| equal, they take equal values when we evaluate them in
| any point. In particular f x x = diag f x, but since diag
| f x = not (f x x), by definition, we have that f x x =
| not (f x x). This is a contradiction since not does not
| have fixed points.
|
| ( I made nat a type variable here since this works for
| any type / set )
| gylterud wrote:
| Bringing in computability from an external point of view
| is a mistake here. Markov had no issue with a. He would
| only disagree with b.
| 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).
| woopsn wrote:
| 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.
| 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.
| JadeNB wrote:
| > 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.
|
| Of course it is likely that an _interesting_ result about
| all positive integers, that is "really" about positive
| integers, is proved by induction, but you certainly don't
| need induction to prove P(n): n = 1.n, or, more boringly,
| P(n): 0 = 0. (These statements are obviously un-
| interesting, both in the human sense of the word and in
| the sense that they are just statements about semi-rings,
| of which the non-negative integers are an example.)
|
| My understanding is that the difference between "For
| every positive integer n, I can prove P(n)" and "I can
| prove [?]n.P(n)" is that the former only guarantees that
| we can come up with some terrible ad hoc proof for P(1),
| some different terrible ad hoc proof for P(2), and so on.
| How could I be sure I have all these infinitely many
| different terrible ad hoc proofs without induction? I
| dunno, but that's all that the first statement
| guarantees. Whereas the second statement, in the context
| of computability, guarantees that there is some
| computable function that takes a positive integer n and
| produces a proof of P(n); that is, there is some sort of
| guaranteed uniformity to the proofs.
|
| I think it may be easier to picture if connected with
| math_comment_21's analogy in
| https://news.ycombinator.com/item?id=44269153: the
| analogous statements in the category of topological
| spaces (I think one actually has to work about topos, but
| I don't know enough about topos theory to speak in that
| language) about a map f : X \to Y are "every element of Y
| has a pre-image under f in X" versus "I can continuously
| select, for each element of Y, a pre-image of it under f
| in X", i.e., "there is a continuous pre-inverse g : Y \to
| X of f."
| fn-mote 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?
|
| Just to be clear to all readers, the axiom of COUNTABLE
| choice is uncontroversial. Nobody is disturbed by
| induction.
|
| The issue it that when you allow UNCOUNTABLE choice -
| choices being made for all real numbers (in a non-
| algorithmic way, I believe - so not a simple formula) -
| there are some unpleasant consequences.
| 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.
| gsf_emergency wrote:
| Careful here, you might wake up the diabol (of pure algebra)
| pfortuny wrote:
| 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 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.
| LudwigNagasena wrote:
| But then you would think there is a right answer to "what
| is true" about categories, and you would face AC again.
| 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.
| bubblyworld wrote:
| Mmm, the problem with computable foundations (in my
| opinion anyway) is that it takes a lot of stuff that is
| trivial in standard foundations (equivalence relations,
| basic operations of arithmetic and their laws, quotients,
| etc) and fills them with subtle logical footguns.
|
| As you say, some view this as a feature, not a flaw. But
| to my mind mathematics is a tool for dissecting problems
| with hard formal properties, and for that I'd like the
| sharpest scalpel I can find.
|
| For me classical foundations strikes a good balance
| between ease of use and subtlety of reasoning required to
| get results. I'm not sure the non-constructive and self-
| referential bits bother me, they don't really get in the
| way unless you're studying logic (in which case you're
| interested in computability and other foundations
| anyway).
| zozbot234 wrote:
| You can use equivalence relations and quotients w/ a
| computable foundation, you just need to rephrase what you
| mean by equality. See e.g. Kevin Buzzard's nice
| explanation at
| https://xenaproject.wordpress.com/2025/02/09/what-is-a-
| quoti...
| bubblyworld wrote:
| Right, I'm aware you _can_ , it's just much trickier to
| do it rigorously. But I suppose that may be more a
| comfort thing. Thanks for the link!
| 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.
| pron wrote:
| > Instead, at worst, he would simply move it from the
| category of being a real formula, to being an ideal
| formula.
|
| No. _No_ result, either ideal or real, may contradict
| reality (it 's just that since infinitary statements do
| not describe reality, they obviously cannot contradict
| it). You can think about it like this: According to
| Hilbert, a valid mathematical foundation is any logical
| theory that is a conservative extension of reality. ZFC,
| constructive foundations, and ultrafinitist foundations
| all satisfy that, so they would all be valid foundations
| according to that principle.
|
| > For example, Euclid's geometry doesn't agree with
| physical reality.
|
| It may not _describe_ physical reality, but it doesn 't
| contradict it.
|
| > 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.
|
| Not only does that disagree with Hilbert's formalism, it
| also disagrees with constructivism. The question of the
| philosophy of mathematics is precisely what, if anything,
| does mathematics describe beyond symbols.
| btilly wrote:
| I have absolutely no idea how physical reality can
| contradict a statement about a formal symbol game.
|
| I am also convinced that what you are saying is not what
| Hilbert actually meant.
|
| But he died before I was born, so I can't ask him.
| Besides, I don't speak German.
| tsimionescu wrote:
| I think what the poster above means is that any formal
| system in which, say, 1 + 1 = 75, even if internally
| consistent as a set of symbols, would not be considered a
| valid logical foundation for mathematics by Hilbert,
| because it directly contradicts physical reality. Of
| course, this is under the assumption that 1 and + and 75
| are meant to have their usual meanings, not that we've
| redefined the + operator to mean "the 73rd successor",
| nor that we're operating in some exotic numerical base
| where 75 is just a different set of symbols to describe
| the number 2.
| pron wrote:
| > I have absolutely no idea how physical reality can
| contradict a statement about a formal symbol game.
|
| Of course it can! For example, if some logic theory
| contains the theorem that a particular realisable
| polynomial-time algorithm that can solve an EXPTIME-hard
| problem, that would contradict physical reality.
|
| I should clarify that when I talk about "physical
| reality" that's shorthand for things that are, at least
| in principle, verifiable using physical means.
|
| > I am also convinced that what you are saying is not
| what Hilbert actually meant. But he died before I was
| born, so I can't ask him. Besides, I don't speak German.
|
| Ok, but if you're not sure what a certain philosophical
| position is, surely you cannot find fault with it. But I
| was able to locate my Heijenoort, so we can try, assuming
| you trust Heijenoort's translation.
|
| So here's just a tidbit from Hilbert's 1925 "On The
| Infinite" (Heijenoort p.367):
|
| _And the net result is, certainly, that we do not find
| anywhere in reality a homogeneous continuum that permits
| of continued division and hence would realize the
| infinite in the small. The infinite divisibility of a
| continuum is an operation that is present only in
| ourthoughts; it is merely an idea, which is refuted by
| our observations of nature and by the experience gained
| in physics and chemistry._
|
| And here are parts of Hilbert, 1927, "The foundations of
| mathematics" (Heijenoort p.464):
|
| _All the propositions that constitute mathematics are
| converted into formulas, so that mathematics proper
| becomes an inventory of formulas._
|
| _...even elementary mathematics contains, first,
| formulas to which correspond contentual communications of
| finitary propositions (mainly numerical equations or
| inequalities, or more complex communications composed of
| these) and which we may call the real propositions of the
| theory, and, second, formulas that -just like the
| numerals of contentual number theory - in themselves mean
| nothing but are merely things that are governed by our
| rules and must be regarded as the ideal objects of the
| theory._
|
| _These considerations show that, to arrive at the
| conception of formulas as ideal propositions, we need
| only pursue in a natural and consistent way the line of
| development that mathematical practice has already
| followed till now._
|
| _... Now the fundamental difficulty that we face here
| can be avoided by the use of ideal propositions. For, if
| to the real propositions we adjoin the ideal ones, we
| obtain a system of propositions in which all the simple
| rules of Aristotelian logic hold and all the usual
| methods of mathematical inference are valid._
|
| _... To be sure, one condition, a single but
| indispensable one, is always attached to the use of the
| method of ideal elements, and that is the proof of
| consistency; for, extension by the addition of ideal
| elements is legitimate only if no contradiction is
| thereby brought about in the old, narrower domain, that
| is, if the relations that result for the old objects
| whenever the ideal objects are eliminated are valid in
| the old domain._
|
| _... To make it a universal requirement that each
| individual formula then be interpretable by itself is by
| no means reasonable; on the contrary, a theory by its
| very nature is such that we do not need to fall back upon
| intuition or meaning in the midst of some argument. What
| the physicist demands precisely of a theory is that
| particular propositions be derived from laws of nature or
| hypotheses solely by inferences, hence on the basis of a
| pure formula game, without extraneous considerations
| being adduced. Only certain combinations and consequences
| of the physical laws can be checked by experiment just as
| in my proof theory only the real propositions are
| directly capable of verification._
|
| _The value of pure existence proofs consists precisely
| in that the individual construction is eliminated by them
| and that many different constructions are subsumed under
| one fundamental idea, so that only what is essential to
| the proof stands out clearly; brevity and economy of
| thought are the raison d 'etre of existence proofs. _
|
| In other words, "ideal" propositions may mean nothing _in
| and of themselves_ but they are valid as long as they are
| a conservative extension of the "real" propositions (the
| narrower domain), which are necessarily meaningful as
| they are "directly capable of verification".
| btilly wrote:
| > Of course it can! For example, if some logic theory
| contains the theorem that a particular realisable
| polynomial-time algorithm that can solve an EXPTIME-hard
| problem, that would contradict physical reality.
|
| It would only contradict physical reality if a machine to
| calculate that algorithm failed to solve the EXPTIME-hard
| problem as promised. And if it failed to do that, I am
| confident that the problem is a mistake in the logic
| theory proof.
|
| As for your long quote from Hilbert, I understand it very
| differently from you. He is saying that our interest in
| ideal mathematics starts with real mathematics. But ideal
| mathematics is something to engage with on its own terms,
| whether or not it corresponds with anything real.
|
| Basically he's just saying, "Math is a formal game.
| People got interested in this game because part of the
| game corresponds to things we experience in reality." But
| that doesn't mean that the game itself depends in any way
| upon physical reality - it exists in its own terms.
| pron wrote:
| > And if it failed to do that, I am confident that the
| problem is a mistake in the logic theory proof.
|
| You can axiomatically add oracles without introducing
| logical inconsistencies. It is commonly done in
| complexity theory. The "mistake" is in interpreting such
| results as directly corresponding to the real world (same
| as interpreting 2 + 1 = 0 in modular arithmetic as if it
| were saying something about natural numbers). That is
| Hilbert's point: we need to be clear about how we map
| certain mathematical statements to the real world, and
| "to make it a universal requirement that each individual
| formula then be interpretable by itself is by no means
| reasonable", i.e. even when we're clear about such a
| mapping, it is not a requirement that _every_ forumla had
| such a mapping. Or, perhaps more clear, Hilbert 's point
| is that if in a logical theory not every formula can be
| assigned a "real meaning", that does not invalidate
| assigning real meaning to some formulas.
|
| > Basically he's just saying, "Math is a formal game.
| People got interested in this game because part of the
| game corresponds to things we experience in reality." But
| that doesn't mean that the game itself depends in any way
| upon physical reality - it exists in its own terms.
|
| He is very explicit that he is _not_ saying that about
| the "real" propositions. He calls them "contentual", as
| in carrying content beyond the symbols. From the same
| talk:
|
| _If we now begin to construct mathematics, we shall
| first set our sights upon elementary number theory; we
| recognize that we can obtain and prove its truths through
| contentual intuitive considerations. The formulas that we
| encounter when we take this approach are used only to
| impart information._
|
| He is very clear that the justification for the use of
| formulas that are "just a symbols game" is that they are
| consistent with formulas that are contentual and are not
| just a symbols game. That is the debate between Hilbert
| and Brouwer, or formalism and intuitionism: whether or
| not _all_ formulas must have an intuitive meaning (
| "content"). In formalism, not all of them must.
|
| It is precisely because Hilbert's justification was based
| on consistency, as without it, "real" propositions could
| be wrong, that the incompleteness results made that
| justification unprovable.
| 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.
| practal wrote:
| Godel's incompleteness theorem tells you why it is a good
| idea to separate semantics (notion of truth) from syntax
| (reasoning). Because some things are true, although you
| cannot prove that they are.
|
| Some people now put forward from this the idea that for the
| natural numbers we know, it is NOT either true or false if
| for example the twin prime conjecture holds. That is
| nonsense. It is just that our methods of proof are strictly
| weaker than our notion of truth is.
|
| That this is so is not even surprising! It is a fact of life
| that what is true is not necessarily what you can prove to be
| true. Innocent people imprisoned are an example of that.
| Guilty people going free another. What is maybe surprising is
| that what is true in what we perceive as the "real world" is
| also true in mathematics, which we imagine to be an "ideal
| realm". But mathematics is ALSO part of the "real world"; if
| you understand this, it is not so surprising. Yes, I am a
| platonist, and I think that everybody who isn't is just plain
| wrong and confused.
|
| Intensional functions are just a special case of extensional
| functions. Where extensional functions are defined on
| _mathematical objects_ , intensional functions are
| extensional functions defined on _representations_ of
| mathematical objects (which are also mathematical objects, by
| the way), but pretend to be acting on the mathematical
| objects themselves, not their representations. That is really
| all there is to it, it is not a deep philosophical mystery.
| To do so can of course be very useful!
| 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
| YetAnotherNick wrote:
| In podcasts or open conversation he is far more critical
| of HoTT.
| zozbot234 wrote:
| Do you have a reference for that, such as a podcast link?
| His paper on Grothendieck's use of equality is
| _implicitly_ rather critical of HoTT proponents ' claims
| anyway (which is why I linked that too), but I'm curious
| to know if he has publicly said anything more specific
| than that.
| YetAnotherNick wrote:
| Go to 2:04:00 at
| https://www.youtube.com/watch?v=0zBDNYRfdlU
|
| > Constructivism is a cancer in my view.
| zozbot234 wrote:
| Thanks for the reference! That take of his sounds a bit
| confused in-context (univalence and constructivism are
| not directly related, you can work non-constructively and
| still use the overall featureset of HoTT/univalence) but
| then his remark about how he's just working on non-
| constructive stuff that we don't even know how to phrase
| constructively is just fair.
|
| Relatedly, the kind of philosophical constructivism that
| would make claims like "non-constructive mathematics is
| just wrong and useless" has been a bit problematic in
| many ways, he's not totally off-base about this.
|
| I disliked his skepticism about proofs-as-programs the
| most, but that's because I think "a _direct_ proof is a
| program " is very much a worthwhile statement. Of course
| some mathematicians will opt not to care about that.
| ncfavier wrote:
| There arguably has been a failure of communication
| between type theorists and "traditional" mathematicians,
| but Buzzard unfortunately has a bit of a history of
| vocally spreading less-than-accurate information about
| type theory. I'd suggest not focusing too much on this
| one person's opinions and engaging with the subject for
| yourself if it interests you.
|
| It's also worth keeping in mind that mathematicians
| traditionally haven't cared too much about foundations,
| and are not necessarily the best people to ask about
| them; see _Hilbert, Bourbaki and the scorning of logic_
| 1. Among people who _are_ interested in foundations
| (logicians, category theorists, computer scientists,
| philosophers, ...), there is a pretty clear consensus
| that HoTT is a major step forward; but of course it 's
| not the kind of "step forward" with immediate, observable
| results. As David Madore puts it, you wouldn't cut the
| roots of an apple tree just because no apples grow there.
|
| [1] https://web.archive.org/web/20210506180228if_/https:/
| /www.dp...
| zozbot234 wrote:
| > but of course it's not the kind of "step forward" with
| immediate, observable results.
|
| Nice, it looks like you agree with Kevin Buzzard's claim
| about HoTT in the presentation I linked above. While
| mathematicians as a whole have historically not cared all
| that much about the practicality of formal foundations,
| it's worth noting that Kevin Buzzard has quite some
| expertise in dealing with the Grothendieck-style fuzzy,
| informal reasoning about equality that happens to be a
| key motivation behind HoTT itself and the univalence
| approach. What he seems to claim on the topic is that
| HoTT makes it a tiny bit easier to phrase a formal
| treatment of these issues, but you still have to do all
| the really hard work of proving that everything
| "respects" the equalities you claim it respects. The fact
| that you can then "transport" mathematical objects,
| proofs etc. along equalities is nifty but is also the
| kind of thing that would be glossed over to begin with in
| any informal treatment, so there's no real gain wrt.
| that.
| 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.)
| thaumasiotes wrote:
| > but you need that you can take a Cartesian product and
| turn it into a set of its elements as well
|
| Huh? In your model, what is a Cartesian product? How can it
| have elements without being a set?
| moomin wrote:
| Well, you'd need some model of index, for one. And I'm
| not sure how you'd construct that with uncountably many
| elements. Even ignoring that, a set containing n elements
| is different from a set containing n sets of one element
| each.
|
| Not saying your formulation is wrong, just that there's a
| fair amount of non-obvious work to get to the classic
| formulation.
| thaumasiotes wrote:
| > Even ignoring that, a set containing n elements is
| different from a set containing n sets of one element
| each.
|
| Different in what way? A set containing n sets of one
| element each is a set containing n elements.
|
| In ZF, everything that's an element of a set is itself a
| set, so unless what's bothering you is the idea that "a
| set containing n elements" might contain the empty set,
| or a set with two elements, I'm not seeing it.
|
| > you'd need some model of index, for one. And I'm not
| sure how you'd construct that with uncountably many
| elements
|
| Why would the number of elements matter? Set elements
| aren't indexed. What are you using your model of index
| for?
|
| I really feel I should repeat the question I asked you to
| begin with: You say you need to convert a Cartesian
| product into a set containing "its elements". In your
| mind, what is a Cartesian product, before that conversion
| takes place?
| moomin wrote:
| Okay, let's simplify. Do we agree that the Cartesian
| product (a,b,c,a) is represented in ZFC as {{1 a} {2 b}
| {3 c} {4 d}} and that that is different from {a b c a}?
| thaumasiotes wrote:
| No. We don't.
|
| Let's note first of all that (a, b, c, a) is a tuple, not
| a Cartesian product.
|
| Where are you getting your ideas from? What do you think
| a Cartesian product is? Give me a definition.
| moomin wrote:
| Ok, I see your problem now. Tuples aren't axiomatic
| components of set theory. Try proving they exist then
| you'll see the problem too.
| thaumasiotes wrote:
| Well, it's true that tuples aren't defined by the ZF
| axioms. They do have a conventional definition, which you
| appear not to know.+
|
| Natural numbers also aren't defined by the ZF axioms; why
| do you think that the definition of a tuple should
| involve them? You're likely to have a hard time finding a
| textbook that agrees.
|
| I'm getting an overwhelming sense here that you don't
| know the meaning of the things you say. If you don't know
| what a Cartesian product is, why do you think it makes
| sense to talk about what you can and can't do with it?
|
| Why do you think it makes sense to write {a b c a}, which
| has no meaning?
|
| + For reference: by the standard convention, the tuple
| (a, b, c, a) is represented as the set {{{a, {a, b}},
| {{a, {a, b}}, c}}, {{{a, {a, b}}, {{a, {a, b}}, c}, a}}.
| You might notice that no numbers appear anywhere. You
| might also notice that regardless of representation - and
| you're free to use other representations - it will never
| be a Cartesian product, because "tuple" and "Cartesian
| product" refer to different things.
| 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
| tel wrote:
| Often it's easy to construct a family of sets representing
| something of interest. For example, we like to define
| integration initially as a finite process of breaking the
| integrand's domain into pieces, computing their area, and
| summing.
|
| To compute the contribution of some piece indexed i, we measure
| the size of its domain, call it the area Ai, and then evaluate
| the integrand, f, at some point xi within that domain, then the
| contribution is Ai * f(xi).
|
| Summing all of these across i produces a finite approximation
| of the integral. Then we take a limit on this process, breaking
| the domain into larger and larger families of sets with smaller
| and smaller areas. At the limit, we have the integral.
|
| This process seems intuitive, but it contains an application of
| the axiom of choice---in the limit, we have an infinite number
| of subsets of our domain and we still have to pick a
| representative xi for each one to evaluate the integrand at.
|
| It's quite obvious how to pick an arbitrary representative from
| each set in a finite family of sets: you just go through one-
| by-one picking an element.
|
| But this argument breaks down for an infinite family. Going
| one-by-one will never complete. We need to be able to select
| these representative xis "all at once". And the Axiom of Choice
| asserts that this is possible.
|
| (Note: I'm being fast-and-loose, but the nature of the argument
| is correct. This doesn't prove integration demands AoC or
| anything like that, just shows how this one sketch of an
| argument would. Specifically, integration normally avoids AoC
| because we can constructively specify our choice function - for
| example, picking the lexicographically smallest point within
| each axis-aligned rectangular cell. Generalize to something
| like Monte Carlo integration, however...)
| john-h-k wrote:
| Bertrand Russell coined an analogy: for any (even infinite)
| collection of pairs of shoes, one can pick out the left shoe
| from each pair to obtain an appropriate collection (i.e. set)
| of shoes; this makes it possible to define a choice function
| directly. For an infinite collection of pairs of socks (assumed
| to have no distinguishing features such as being a left sock
| rather than a right sock), there is no obvious way to make a
| function that forms a set out of selecting one sock from each
| pair without invoking the axiom of choice.
|
| (From Wikipedia but I've always found it good)
| bmacho wrote:
| The single most best definition I know is what is on the
| wiki[0]:
|
| > A choice function (also called selector or selection) is a
| function f, defined on a collection X of nonempty sets, such
| that for every set A in X, f(A) is an element of A. With this
| concept, the axiom can be stated:
|
| > Axiom--For any set X of nonempty sets, there exists a choice
| function f that is defined on X and maps each set of X to an
| element of that set.
|
| I like this definition because IMO it is simple, close to the
| name of the axiom, and you might want to use it in this form,
| that is, having a set of sets, and taking a choice function on
| them.
|
| To understand its importance and the controversies around it,
| you'll need some examples and counterexamples how truthness and
| provability and knowability (regarding structures, numbers,
| metamathematics) interact; also what are the views of the
| majority of working mathematicians and people in other fields
| using mathematics.
|
| [0] : https://en.wikipedia.org/wiki/Axiom_of_choice#Statement
| bmacho wrote:
| Tangential, but a choice function is one of the ur-examples
| of Dependent Type Theory (DTT). In standard ZFC the choice
| function on X would have the type signature
| f: X -> UX (union X).
|
| And you know the additional information that ([?]A:X) (f(A)
| [?] A), which is not encoded in the type signature, just an
| additional fact that you know, and have to keep track of it.
| In DTT the codomain can be the function of the picked element
| of the domain. In this case, the DTT type signature of f
| would be f: (A:X) -> A.
|
| So in this case the signature of the function carries
| strictly more information than in the case of normal, static
| function type signatures in ZFC. And the axiom of choice
| simply states that the type (A:X) -> A is non-empty if every
| A are non-empty.
| munificent wrote:
| The material is way over my head, but, wow, what a beautifully
| designed page. The layout and typography is delightful.
| mietek wrote:
| Thanks! The source code is set in Fabrizio Schiavi's amazing
| PragmataPro.
|
| https://fsd.it/shop/fonts/pragmatapro/
|
| https://github.com/fabrizioschiavi/pragmatapro
| 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?
| nwallin wrote:
| > 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 wrote:
| 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.
| 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-14 23:01 UTC)