Return to Answer

Now, importantly, we distinguish between operations and functions. The latter is a mapping from a set $A$ to a set $B$, and the former 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.

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.

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_2(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))$.

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))$.

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$.

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))$, ...

Sheaves

In geometric models of intutionistic logic, such as the topos of sheaves on a space $X$, the faith of the axiom of choice depends on the topological properties of $X$. In sheaves existence is local: to show that $\exists x \ in A . \phi(x)$ holds in some neighborhood $U \subseteq X$, it suffices to cover $U$ with a family $(U_i)_{i \in I}$ and provide a witness $a_i \in A_{U_i}$ of $\phi(a_i)$ on each element of the cover. Cruicially, there is no requirement that the witnesses $a_i$ be compatible with each other on the overlaps $U_i \cap U_j$, and so they may not be composable into a single witness on $U$. Then, choice may fail because there may be no way to compose together local witnesses of (1) to give a choice function $f$ in (2).

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$.

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))$, ...