Comment by bobbylarrybobby

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

> 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

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

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

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

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