Comment by bobbylarrybobby
1 month ago
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)]`.
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.
The two statements imply each other, they are logically equivalent:
https://en.wikipedia.org/wiki/Product_topology#Axiom_of_choi...
>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.
> 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
> 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.)
> 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?
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.
5 replies →
Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
As far as I understand there's no such thing “undecidable” in absolute, Gödel incompleteness theorem is about being undecidable under a certain set of axioms.