This is about constructive mathematics, but it is not a research question. But since it may also be of interest for research mathematicians, I hope this question is appropriate for this forum. As Andrej Bauer writes in his recent paper Five stages of accepting constructive mathematics:
As exciting as a multiverse of mathematics may be, the working mathematician
has no time to spend their career wandering from one world to another. Nevertheless,
they surely are curious about the newly discovered richness of mathematics,
they welcome ideas coming from unfamiliar worlds, and they strive to make their
own work widely applicable. They will find it easier to accomplish these goals if they
speak the lingua franca of the mathematical multiverse—constructive mathematics.
So, I found a quote by mathematician Errett Bishop I don't quite understand. It says:
A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence.
(Wikipedia refers to the book Constructive analysis by Errett Bishop and Douglas S. Bridges, published in 1985.)
Isn't constructive mathematics all about not asserting that something exists until we can construct a witness? But what the axiom of choice is doing is that it states that there is always a choice function, although we can't always construct one. In view of that fact, I think that the axiom of choice is not constructively justified. Could you clarify what Bishop is trying to say in this quote?
Surprisingly, in 1967 (that's well before he said the quote from above), in one of his books, Bishop gives the exercise to prove that the axiom of choice implies the law of excluded middle. So it seems Bishop knew that the axiom of choice is not constructively valid. How does that match historically with the quote from above?
Best Answer
According to the BHK interpretation of intuitionistic logic we have that:
Here "method" should be understood as an unspecified, pre-mathematical notion. It could be algorithm, or continuous map, or mental process, or Turing machine, etc.
The axiom of choice can be stated, for any sets $A$, $B$ and relation $\rho$ on $A \times B$, as: \begin{equation} (\forall x \in A . \exists y \in B . \rho(x,y)) \Rightarrow (\exists f \in B^A . \forall x \in A . \rho(x, f(x)). \tag{AC} \end{equation} This is equivalent to the usual formulation (exercise, or ask if you do not see why). Let us unravel what it means to have a proof of the above principle. First, a proof of $$\forall x \in A . \exists y \in B . \rho(x,y) \tag{1}$$ is a method $C$ which takes as input $a \in A$ and outputs a pair $$C(a) = (C_1(a), C_2(a))$$ such that $C_1(a) \in B$ and $C_2(a)$ is a proof of $\rho(a, C_1(a)).$ Second, a proof of $$\exists f \in B^A . \forall x \in A . \rho(x, f(x)) \tag{2}$$ is a pair $(g, D)$ such that $g$ is a function from $A$ to $B$ and $D$ is a proof of $\forall x \in A . \rho(x, g(x))$.
Therefore a proof of (AC) above is a method $M$ which takes the method $C$ which proves (1) and outputs a pair $(f, D)$ which proves (2). Is there such an $M$? It looks like we can take $f = C_1$ and $D = C_2$, and viola the axiom of choice is proved constructively! Well, not quite. We were asked to provide a function $f : A \to B$ but we provided a method $C_1$. Is there a difference? That depends on the exact meaning of "method" and "function". There are several possibilities, see below.
The important thing is that now we can understand what Bishop meant by "a choice is implied by the very meaning of existence". If we ignore the difference between "method" and "function" then under the BHK interpretation choice holds because of the constructive meaning of $\exists$: to exist is to construct, and to construct a $y \in B$ depending on $x \in A$ is to give a method/function that constructs, and therefore chooses, for each $x \in A$ a particular $y \in B$.
It remains to consider whether a "method" $C_1$ taking inputs in $A$ and giving outputs in $B$ is the same thing as a function $f : A \to B$. The answer depends on the exact formal setup that we use to express the BHK interpretation:
Martin-Löf type theory
In Martin-Löf type theory there is no difference between "method" and "function", and therefore choice is valid there (but the exact argument outlined above).
Bishop constructive mathematics
In Bishop constructive mathematics a set is given by an explanation of how its elements are constructed, and when two such elements are equal. For instance, a real number is constructed as sequence of rational numbers satisfying the Cauchy condition, and two such sequences are considered equal when they coincide in the usual sense. This means, in particular, that two different constructions may represent the same element (both $n \mapsto 1/n$ and $n \mapsto 2^{-n}$ represent the real number "zero").
Now, importantly, we distinguish between operations and functions. The former is a mapping from a set $A$ to a set $B$, and the latter a mapping which respects equality (we say that it is extensional). To see the difference, consider the operation from $\mathbb{R}$ to $\mathbb{Q}$ which computes from a given $x \in \mathbb{R}$ a rational $q \in \mathbb{Q}$ such that $x < q$: since $x$ is a Cauchy sequence, we may take $q = x_i + 42$ for a large enough $i$ (which can be determined explicitly once we make our definition of reals a bit more specific). The operation $x \mapsto q$ does not respect equality: by taking a different Cauchy sequence $x'$ which represents the same real, we get a rational upper bound $q'$ which is not equal to $q$. In fact, in Bishop constructive mathematics it is impossible to construct an extensional operation that computes rational upper bounds of reals.
In Bishop constructive mathematics method is understood as operation, and function as extensional operation. Choice is then valid only in some instances, but not in general. In particular, if $A$ has the property that every element is canonically represented by a single construction, then every operation from $A$ to $B$ is automatically extensional, and choice from $A$ to $B$ is valid. An example is $A = \mathbb{N}$ because each natural number is represented by precisely one construction: $0$, $S(0)$, $S(S(0))$, ...
The moral of the story is that the devil hides important details in the passage from informal, pre-mathematical notions to their mathematically precise formulation.