4 ms·

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.

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.

deleted 1y ago
[deleted]
throw310822 1y ago
Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?
- littlestymaar 1y ago
  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.
moefh 1y ago
> 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 https://en.wikipedia.org/wiki/Chaitin%27s_constant
- deleted 1y ago
  [deleted]
SabrinaJewson 1y 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. 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 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 https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.
- deleted 1y ago
  [deleted]
- gjm11 1y ago
  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 1y ago
  The two statements imply each other, they are logically equivalent: https://en.wikipedia.org/wiki/Product_topology#Axiom_of_choice 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.
moomin 1y ago
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 1y ago
  > 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 1y ago
    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 1y ago
      > 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 1y ago
drdec 1y ago
> 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 1y ago
> 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.

deleted 1y ago

[deleted]

throw310822 1y ago

Isn't that equivalent (or, ok, similar) to saying that we can decide undecidable mathematical truths?

littlestymaar 1y ago
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.

moefh 1y ago

> 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 https://en.wikipedia.org/wiki/Chaitin%27s_constant

deleted 1y ago
[deleted]

SabrinaJewson 1y 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. 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 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 https://ncatlab.org/nlab/show/bracket+type)) would just be `λ [a] ↦ λ [b] ↦ [(a, b)]`.

deleted 1y ago
[deleted]
gjm11 1y ago
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 1y ago
The two statements imply each other, they are logically equivalent: https://en.wikipedia.org/wiki/Product_topology#Axiom_of_choice 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.

moomin 1y ago

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 1y ago
> 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 1y ago
  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 1y ago
    > 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 1y ago

drdec 1y ago

> 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 1y ago

> 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.