On Sun, Apr 27, 2014 at 5:48 PM, Gareth McCaughan <gareth.mccaughan@pobox.com> wrote:
On 28/04/2014 00:31, Mike Stay wrote:
If that's the case, I don't see why it's not constructive: in order to demonstrate that the sets you're taking the product over are nonempty, you have to construct at least one element of each.
Nope. You can prove a set is nonempty without constructing any elements.
How?
Once you've got the elements, constructing the list is trivial.
Nope. If what you constructed was, say, an unordered pair of undistinguished elements of each set, getting an element in the cartesian product requires a set that performs the function of choosing one element from each pair.
(If you have infinitely many pairs of shoes, you don't need AC to get one shoe from each pair, because you can e.g. take the left shoe from each. But if you have infinitely many pairs of socks, you do need AC because there is no distinction between left and right socks.)
OK, that makes sense. -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com