← Back to context

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)]`.

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