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.
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.
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.
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?
How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.
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.
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.
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.
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.
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.
> 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
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.
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.
Gödel'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!
> 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?)
> 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.
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.
- 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.
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?
That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from.
The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8).
Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.
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?
> 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.
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.
> 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 × B)` (supposing that `Nonempty` is defined as the [bracket type](https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.
> 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.
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.)
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.]
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.
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 ℕ of them), but how the fuck do you order water (assuming it's like ℝ — there are no molecules and you can divide every drop infinitely many times)?
This is both why we have it — ℝ 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.
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.
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.
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...)
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.
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).
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.
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.
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.
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.
8 replies →
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?
19 replies →
How is it different from using ZF as a meta-theory to study ZF(C)? Is there anything special about category theory vis-à-vis ZF as a meta-theory? You're not arguing about ontology or the nature of truth, because you've picked category theory as your ontology just like you could pick ZF or ZFC.
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.
2 replies →
Doesn't "continuous" make all the difference here? AC doesn't contain a comparable limitation, so the analogy doesn't work that week.
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.
Careful here, you might wake up the diabol (of pure algebra)
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.
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://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.
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:
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
with:
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:
1 reply →
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.
1 reply →
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.
24 replies →
Gödel'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!
> 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?)
1 reply →
> 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.
2 replies →
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.
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
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?
That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as Martin-Löf does, then the function you get should be extensional with respect to the relevant setoid structures, which is where the power of the axiom comes from.
The modern view on this is homotopy type theory, where types themselves are intrinsically seen as ∞-groupoids (a higher analogue of setoids) and ∃ is interpreted as a propositionally truncated Σ-type (see chapter 3 of the HoTT book). In this setting the axiom of choice says that for any set X, (∀ (x : X). ∥ P x ∥) → ∥ ∀ (x : X). P x ∥ (see section 3.8).
Note that from the perspective of homotopy type theory, Zermelo's axiom of choice is too strong: it is equivalent to global choice (for all types A, ∥ A ∥ → A), which is inconsistent with univalence.
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?
7 replies →
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.)
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.
> 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.
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.
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.
Can you really reassemble them into something bigger or just into more copies of the same size?
I've never quite gotten the axiom of choice. Can anyone ELI5?
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.
> 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 × B)` (supposing that `Nonempty` is defined as the [bracket type](https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.
3 replies →
> 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
1 reply →
> 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.
> 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.
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.)
7 replies →
Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
1 reply →
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.]
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)
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 ℕ of them), but how the fuck do you order water (assuming it's like ℝ — there are no molecules and you can divide every drop infinitely many times)?
This is both why we have it — ℝ 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
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
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
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
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.
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...)
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).
Note that this proof doesn't require the axiom of choice, only excluded middle.
AC is much stronger than excluded middle. This doesn't really say anything about what AC does.
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.
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
- Gödel's sandbox for containing the axiom
Yes. Here’s a great ELI5 intro:
https://youtu.be/_cr46G2K5Fo?si=Q6iEm3m-Nyge3FUW
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).
The material is way over my head, but, wow, what a beautifully designed page. The layout and typography is delightful.
Thanks! The source code is set in Fabrizio Schiavi’s amazing PragmataPro.
https://fsd.it/shop/fonts/pragmatapro/
https://github.com/fabrizioschiavi/pragmatapro
[flagged]
[flagged]
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.
It is not about real world, choosing an axiom set must simply put produce something valid (with no contradictions) and that is not trivial.
3 replies →