On Mon, Apr 28, 2014 at 7:45 AM, Andy Latto <andy.latto@pobox.com> wrote:
On Sun, Apr 27, 2014 at 11:28 PM, Mike Stay <metaweta@gmail.com> wrote:
On Sun, Apr 27, 2014 at 6:22 PM, Adam P. Goucher <apgoucher@gmx.com> wrote:
Nope. You can prove a set is nonempty without constructing any elements.
How?
For example, let S be the set of well-orderings of the reals. This is non-empty, but you can't construct any of its elements.
Ah, well I (as a constructivist) wouldn't say the set is non-empty, then. But I can see how if you are only able to construct two or more elements of each set, then there may not be a way to pick one.
To take a simpler but closely related example, let S be the non-empty subsets of the reals. Can you specify for me an element chosen from each non-empty subset of the reals? Or would you as a constructivist not say that all of the non-empty subsets of the reals are non-empty?
To construct S, one would have to provide a constructive proof that each of its elements is nonempty. In most cases, it's at least conceivable that the only thing one can construct is a pair of undistinguished points, from which there's no way to choose just one, so I can see how you'd still need AC's magic to provide a choice function. -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com