|
On one level, this one is relatively easy to answer: the full Axiom of Choice (AC),
(1)
∀x∈X ∃y∈Y P(x,y) ⇒ ∃� ∈Y X ∀x∈X P(x,� (x)),
implies the Law of Excluded Middle (LEM), as was shown by Diaconescu [15] and later by Goodman�Myhill [17]. Contrary to a popular misconception that a dislike of, or disbelief in, AC is the reason why people do constructive mathematics, it is not AC, but LEM, that is the primary object of suspicion; However the fact that AC implies LEM confirms one�s instinct that AC is nonconstructive.
In view of the Diaconescu�Goodman�Myhill theorem, what did Bishop mean when he said that under the hypotheses of (1),
"A choice function exists � because a choice is implied by the very meaning of existence"?
I believe that he meant that the constructive interpretation of the hypothesis in (1) is that there is an algorithm which leads us from elements x of X to elements y of Y such that P(x,y) holds. However, to compute the y from a given x, the algorithm will use not just the data describing x itself, but also the data proving that x satisfies the conditions for membership of the set A. Thus the algorithm will not be a function of x but a function of both x and its certificate of membership of A. The value at x of a genuine function from X to Y would depend only on x and not on its membership certificate.
At a deeper level, the question is tricker to answer, at least if recast in the form, �What, if any, choice axioms are permissible in constructive mathematics?�. Some constructive mathematicians, notably Fred Richman, doubt the constructive validity of even countable choice (and hence of dependent choice). The argument in favour of countable choice is that one has to do no work to show that a natural number x belongs to the set N of natural numbers: each natural number is, as it were, its own certificate of membership of N. Thus in the case X = N, the choice algorithm implied �by the very meaning of existence� in (1) is, in fact, a genuine function on N. Needless to say, those who distrust even countable choice as a constructive principle do not buy into this argument.
|
