Bishop quote stating that axiom of choice is constructively valid

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?

• I can explain but need to feed the kids first. – Andrej Bauer Jan 24 '17 at 18:38
• The axiom of choice says that there exists a choice function for any family of inhabited sets. The hypothesis here is that, for each of the sets in question, there exists an element. When you interpret "for all ... there exists" constructively in this hypothesis, that interpretation amounts to the existence of a choice function. (I've glossed over a lot, in the hope of conveying the essential idea, so watch for Andrej's answer to clarify things.) – Andreas Blass Jan 24 '17 at 18:45
• A friend of mine gave me this link: michaelt.github.io/martin-lof/… – user104007 Jan 24 '17 at 20:04
• The term "constructive mathematics" is used with related but subtly different meanings. The lingua franca of the mathematical multiverse is "intuitionistic logic" (classical logic is intuitionistic logic plus the axiom of excluded middle). Sometimes "constructive mathematics" refers to doing mathematics using only intuitionistic logic. But sometimes "constructive mathematics" refers to one of several specific schools, where some further axioms are used (for instance Markov's principle or the anti-classical axiom that any function $\mathbb{R}\to\mathbb{R}$ is continuous). – Ingo Blechschmidt Jan 25 '17 at 16:51

According to the BHK interpretation of intuitionistic logic we have that:

1. A proof of $\exists x \in A . \phi(x)$ consists of a pair $(a, p)$ where $a \in A$ and $p$ is a proof of $\phi(a)$.
2. A proof of $\forall x \in A . \phi(x)$ is a method which takes as input $a \in A$ and outputs a proof of $\phi(a)$.
3. A proof of $\psi \Rightarrow \xi$ is a method which takes proofs of $\psi$ to proofs of $\xi$.

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: $$(\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}$$ 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.

• That's a very good formulation of the axiom of choice. Quite frankly when I hear the axiom of choice in its original formulation, I question it. But when I hear it in different equivalent formulations, it seems much more intuitive and clear. This formula is a great one. For some reason it reminds me of the implicit function theorem... – user78249 Jan 25 '17 at 1:29
• Another way to understand the formula is that every total relation contains a function. – Andrej Bauer Jan 25 '17 at 6:04
• Did you mean that (for Bishop), functions must be extensional but operations (like the one from $\mathbb R$ to \mathbb Q\$ producing an upper bound) need not? If so, then "latter" and "former" are reversed in the sentence introducing the distinction. – Andreas Blass Jan 26 '17 at 14:42
• Thanks, I've always found it challenging to tell which is which. – Andrej Bauer Jan 26 '17 at 17:40