THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS)

Abstract

There seems to be a view that intuitionists not only take the Axiom of Choice (AC) to be true, but also believe it a consequence of their fundamental posits. Widespread or not, this view is largely mistaken. This article offers a brief, yet comprehensive, overview of the status of AC in various intuitionistic and constructivist systems. The survey makes it clear that the Axiom of Choice fails to be a theorem in most contexts and is even outright false in some important contexts. Of the systems surveyed, only intensional type theory renders AC a theorem, but the extent of AC in that theory does not include, for instance, real analysis. Only a small amount of extensionality is required in order for the obvious proof an intuitionist might offer for AC to break down.

1 An illusion?

There may be an illusion, even among philosophical friends of mathematical constructivism and intuitionism, that intuitionists not only take familiar Axiom(s) of Choice (AC) to be true, but also believe them a consequence of their fundamental posits. This may be due to remarks like these:¹

This axiom is unique in its ability to trouble the conscience of the classical mathematician, but in fact it is not a real source of the unconstructivities of classical mathematics. A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence. [9, p. 9]

To be sure, unqualified sentiments like this are not often expressed in print, and our impression that the view is widespread is anecdotal, based on offhand remarks that should not be quoted. Nevertheless, a survey of the state of AC in intuitionistic and constructive mathematics may be in order. Our purpose here is to demonstrate that, whether it is widespread or not, the perspective is largely mistaken. An array of articles, books, and research reports show that, in general, AC is false, and intuitionists know that. Its falsity follows directly from precepts reasonably basic to the mathematics of the movement(s). This was as much the case for the primordial Dutch intuitionists, L. E. J. Brouwer and Arend Heyting, as it is for the intuitionists and constructivists of today—despite a wide range of differences among intuitionists and constructivists on a variety of mathematical and philosophical matters.

None of the results presented here are new. All are known in sundry parts of the field. In constructive and intuitionistic mathematics today, there is an extensive literature on axioms of choice, and a large range of formal theories that either include or exclude forms of those axioms. Without claiming to be comprehensive, we draw a battery of results together to lodge some general points to dispel any illusion that AC in general is—and must be—unqualifiedly true intuitionistically.²

The phrase “in most contexts” in our title is a nod to certain facts. First, the general version of AC before us is, as in classical mathematics, multiply extensional—applying to extensional collections and relations, and employing extensional functions required to preserve identity. There are forms of AC that are, in one way or several, intensional. As we shall see, such forms of AC may at times hold intuitionistically when extensional AC fails.

Accordingly, the arguments of the early sections in this article rely upon a variety of what may be called “extensionality assumptions.” Without those assumptions, the arguments usually will not go through. One way of understanding the nature of such extensionality assumptions will be presented in Section 7. See also Bell’s book [8], which contains a painstaking analysis of the situation.

Moreover, there are effective versions of AC, such as intuitionistic Church’s Thesis, in which the relevant functions are computable. We will take some of these up in the penultimate section.

2 What is “the” Axiom of Choice?

In both classical and intuitionistic or constructive mathematics, there are many genera and species of Axioms of Choice: local, global, for sets, for classes, for types, over whole universes, countable, uncountable, dependent, relativized dependent, intensional, extensional, and so on. For immediate purposes, we focus on one particular statement of the axiom. It covers a goodly range of the contested territory, though not all of it.

In these definitions, we apply the term “collection” in as neutral a way as possible to cover classes, sets, species, and types, at least. Differences between these kinds of collections will become apparent as we go.

Definition $A \Rightarrow B$ , Axiom of Choice or AC, base, choice function

1. 1. For collections A and B, $A \Rightarrow B$ is the collection of all total functions mapping A into B.

2. 2. The Axiom of Choice (AC) is the statement that, for all collections A and B, and all suitable relations $R(x,y)$ ,

   if $\forall x \in A \ \exists y \in B \ R(x, y)$ , then there is a function $f \in (A \Rightarrow B)$ such that $\forall x \in A \ R(x, f(x)).$

3. 3. If a collection A satisfies AC for all B and all suitable R, then A is called a base. Consequently, one can express AC by asserting that every collection is a base.

4. 4. When a function $f \in (A \Rightarrow B)$ satisfies the consequent of AC, f is known as a choice function.

When focus is on a first-order theory, AC is often expressed as a scheme:

if $\forall x \in A \ \exists y \in B \ \phi (x, y)$ , then there is a function $f \in (A \Rightarrow B)$ such that $\forall x \in A \ \phi (x, f(x)),$

where $\phi (x,y)$ is a suitable formula.

We assume that we have a notion of identity on the elements of any collection. We may therefore formulate the condition of functionality, or single-valued-ness, which every function $f\in (A\Rightarrow B)$ must satisfy: for all $a,b\in A$ , if $a=b$ , then $f(a)=f(b)$ . Functions thus preserve identity. Following Bishop, we call a transformation from one collection to another that need not preserve identity an operation. The difference between the notions of function and operation will loom quite large.

3 Traditional Brouwerian intuitionism and AC

An old-time intuitionist, perhaps an early disciple of Brouwer, would easily have been able to recognize that AC is false in general—that some collections essential to intuitionism cannot be bases.

We shall take for granted the definition of real numbers in terms of Cauchy sequences going back to Méray and Cantor that is standardly assumed in constructive mathematics.

Definition Real number, less than

1. 1. A real number is an equivalence class of Cauchy sequences r of rational numbers with moduli functions $\mu $ : for each natural number k, for all $m, n \geq \mu (k)$ , $|r(m) - r(n) | < 2^{-k}$ . The pertinent equivalence relation is that of co-convergence. The associated equivalence class of r is $[r]$ .

2. 2. The collection of all real numbers, denoted $\mathbb {R}$ , is

   $$ \begin{align*}\{ [r]: r \text{ is a Cauchy sequence}\}.\end{align*} $$

3. 3. A real number $[r]$ is less than a real number $[s]$ , in symbols, $[r] < [s]$ , whenever there is a k and an m such that, for all $n \geq m$ , $s(n) - r(n)> 2^{-k}$ . This definition is independent of the choice of representatives r and s.

We thus intend our use of the term “collection” to be such that the natural numbers and the real numbers both form a collection, denoted $\mathbb {N}$ and $\mathbb {R}$ , respectively.

Note that traditional intuitionists did indeed countenance a collection embracing all real numbers:

All real numbers form a species $\ldots $ This species is the (one-dimensional) continuum (of real numbers). [25, p. 38]

We then call upon a simple consequence of Brouwer’s Continuity Theorem ([13, p. 66], [25, p. 46]), which is a hallmark of traditional intuitionism. The Continuity Theorem states that

every total function from $\mathbb {R}$ into $\mathbb {R}$ is continuous.

Because $\mathbb {N}$ carries the discrete topology, it follows at once that

every total function from $\mathbb {R}$ into $\mathbb {N}$ is constant.

For a natural number n we write $\overrightarrow {n}$ for the sequence that is constantly n, i.e., $\overrightarrow {n}(m)=n$ for all m. Using $\overrightarrow {n}$ , we can make sense of relations between real numbers and natural numbers. For instance, $x<n$ can be taken to mean $x<[\overrightarrow {n}]$ .

Lemma. For each real number $[r]$ , there is a natural number n such that $[r] < n$ .

Proof Let Cauchy sequence r have modulus $\mu $ . Let k be $1$ , and calculate $\mu (1)$ . Since r is a Cauchy sequence, $r(\mu (1))$ is a rational number. From the definition of Cauchy sequence, we know that, for all $m> \mu (1)$ , $|r(\mu (1))-r(m)| < 1/2$ . So after $\mu (1)$ , the value of $r(m)$ never leaves the open interval between $r(\mu (1))-\frac {1}{2}$ and $r(\mu (1))+\frac {1}{2}$ , no matter how large m gets. The terms of any Cauchy sequence co-convergent with r can be bounded similarly. Now, take n to be any natural number that is at least two larger than $r(\mu (1))$ . Plainly, $[r] < n$ .

Theorem. The collection of real numbers $\mathbb {R}$ is not a base. Hence, AC is false in general.

Proof The argument is sketched by Troelstra and van Dalen [51, pp. 189–190]. Assume that AC holds or, at minimum, that the collection of real numbers, $\mathbb {R}$ , is a base. By the above Lemma, the formula $\forall x \in \mathbb {R}\ \exists n\in \mathbb {N}\ x<n$ holds, and hence by AC there is a choice function $f\in (\mathbb {R} \Rightarrow \mathbb {N})$ with the property that, for each $[r]$ in $\mathbb {R}$ , we have $[r] < f([r])$ .

Since $[\overrightarrow {f([r])}]$ is a real number, we may apply f to it, obtaining

$$\begin{align*}[r] < f([r]) < f([\overrightarrow{f([r])}]). \end{align*}$$

This shows that f is not a constant function, contradicting Brouwer’s Continuity Theorem. Hence, $\mathbb {R}$ is not a base, and AC is false.

From the Lemma and AC we are thus led to assert the existence of a function $f\in (\mathbb {R}\Rightarrow \mathbb {N})$ such that $x<f(x)$ holds for every $x\in \mathbb {R}$ . In the proof of the Lemma, we prove the existence of a function $g\in (\mathbf {Cauchy}\Rightarrow \mathbb {N})$ such that $[r]<g(r)$ holds for every $r\in \mathbf {Cauchy}$ . Since the existence of f contradicts Brouwer’s Continuity Theorem, one might well wonder why the existence of g does not? It does not, since g is a function on Cauchy sequences, whereas Brouwer’s Continuity Theorem concerns functions on $\mathbb {R}$ .

The proof of the Theorem in effect shows that the intuitionist cannot hope that the function g constructed in the Lemma induces a function ${\overline {g}\in (\mathbb {R}\Rightarrow \mathbb {N})}$ . In particular, she cannot hope to prove that $g(r)=g(s)$ whenever r and s are co-convergent Cauchy sequences. Nor would it be acceptable for her to define a function $\overline {g}\in (\mathbb {R}\Rightarrow \mathbb {N})$ as a composition,

$$\begin{align*}x\mapsto u(x)\mapsto g(u(x)),\end{align*}$$

where $u(x)$ is a unique representative from the equivalence class x of co-convergent Cauchy sequences. The principle that unique representatives may always be picked out from equivalence classes is itself an extensional choice principle [30, 36].

In Bishop’s terminology, the function g constructed by the Lemma induces an operation on $\mathbb {R}$ , but not a function. The Axiom of Choice, however, requires a function.

4 Intuitionistic set theory and AC

Constructivists who are not intuitionists avoid LEM in their mathematical work, but refrain from affirming its out-and-out invalidity. In contrast, intuitionists who trace their intellectual lineage back to Brouwer insist that LEM is invalid, in symbols:

$$ \begin{align*}\neg \forall p \ (p \vee \neg p).\end{align*} $$

Given this, any intuitionist who accepts even a tiny dose of set theory can prove in a moment that AC is false. By a result in topos theory of Diaconescu [17], AC entails LEM in the so-called internal language of toposes, which is a form of higher-order intuitionistic logic.³ Goodman and Myhill [22] proved the more concrete result that, in a set theory containing the axioms of extensionality and pairing, $\phi \vee \neg \phi $ follows constructively from AC for every formula $\phi $ such that the formula $x=0\wedge \phi $ can be used for separating out a subset from a given set. In particular, in a set theory containing the axioms of extensionality and pairing and admitting full separation, AC entails LEM.

The strategy of the Goodman–Myhill proof is to use AC to show that identity between sets is decidable and then note that every formula $\phi $ is equivalent to an identity, $a=b$ , between sets. We take it for granted that the natural numbers $0$ and $1$ exist, with $0 \neq 1$ .

Theorem Goodman and Myhill

For any sets a and b, $\{ a, b \}$ is a base if and only if identity is decidable on $\{ a, b \}$ , i.e., $a = b$ or $a \neq b$ .

Proof Assume that $\{ a, b \}$ is a base. Let $R(x, y)$ be the binary relation where

$$\begin{align*}R(x, y) \text{ if and only if } (x = a \text{ and } y = 0) \text{ or } (x = b \text{ and } y = 1).\end{align*}$$

Clearly,

$$\begin{align*}\forall x \in \{ a, b \} \ \exists y \in \{ 0 , 1 \} \ R(x, y).\end{align*}$$

Since $\{ a , b \}$ is a base, there is a choice function f with domain $\{ a, b \}$ such that

$$\begin{align*}\forall x \in \{ a, b \} \ \big(f(x) \in \{ 0 , 1 \} \wedge R(x, f(x))\big).\end{align*}$$

Since identity is decidable on $\{ 0, 1\}$ , there are four possible cases:

1. 1. $f(a) = 0$ and $f(b) = 0$ ,

2. 2. $f(a) = 1$ and $f(b) = 1$ ,

3. 3. $f(a) = 0$ and $f(b) = 1$ ,

4. 4. $f(a) = 1$ and $f(b) = 0$ .

In cases 1 and 2, use the definition of $R(x,y)$ to find $a=b$ . In cases 3 and 4, use the functionality of f to find $a\neq b$ .

Since the cases are exhaustive, it follows that $a = b$ or $a \neq b$ .

The converse—that $\{ a , b \}$ is a base provided that identity is decidable on $\{ a, b \}$ —follows immediately: when identity is decidable on $\{ a, b \}$ , then the latter set is in bijective correspondence with the finite set $\{ 0, 1 \}$ .

Under minimal assumptions, an intuitionist may now infer the following corollary.

Corollary. AC is false.

Proof Assume AC. There are at least two ways for an intuitionist to derive a contradiction.

First, assume that we may form the unordered pair $\{r,s\}$ of real numbers r and s. By the Theorem, identity on $\{r,s\}$ is decidable. This, however, allows us to define a discontinuous function on $\mathbb {R}$ , contrary to Brouwer’s Continuity Theorem (see Section 3).

Second—the way of Goodman and Myhill—let $\phi $ be a formula such that

$$\begin{align*}\{x\in\{0,1\} \,|\,x=0\wedge \phi\}\end{align*}$$

is a set. Whenever $\phi $ is a formula in the signature $\{\in , =\}$ this will be a set according to any set theory that admits full separation. Let us call the set in question $A_{\phi }$ . Since $A_{\phi }$ and $\{0\}$ are sets (the latter by pairing), we may form the set $\{A_{\phi }, \{0\}\}$ by pairing and use the Theorem together with AC to find that

$$\begin{align*}A_\phi=\{0\}\end{align*}$$

is decidable. Owing to the equivalence

$$\begin{align*}\phi \leftrightarrow (A_\phi = \{0\}),\end{align*}$$

it follows that also $\phi $ is decidable. If $\phi $ is allowed to be arbitrary, LEM therefore holds in the set-theoretical universe. But, as already noted, LEM is false for an intuitionist.

The only set-theoretic principle used in the proof of the Theorem is that of unordered pairing (and, of course, that $0\neq 1$ ), which is certainly intuitionistically acceptable, if any set-theoretic principle is. An intuitionist therefore needs only the admission that an unordered pair $\{r,s\}$ of real numbers exists to conclude that AC is false. This is the first of the two proofs of the Corollary.

The second proof—Goodman and Myhill’s—also uses unrestricted separation. Call a formula in the signature $\{\in , =\}$ restricted if all of its quantifiers are bounded, i.e., of the form $\forall x\in a$ or $\exists x\in a$ . As we shall see in the next section, some well-known constructive set theories admit only restricted formulas in instances of the Axiom of Separation. In such systems, the Goodman–Myhill proof delivers LEM for restricted formulas. Tennant [47, 48] argues that a constructivist must restrict separation to decidable properties: for $\phi (x)$ to be used in separating out a subset of a, the formula $\phi (b)\vee \neg \phi (b)$ must be derivable for every $b\in a$ . Under this restriction, the Goodman–Myhill proof yields only the tautology that LEM holds for decidable formulas. This point is nicely illustrated by the intuitionistic small set theory of , Shapiro, and Rathjen [38], where AC is a theorem, but only decidable separation is provable.

Again it is essential that the choice function f invoked in the proof of the Theorem is indeed a function and not an operation: the functionality of f is appealed to, not only when we infer $a\neq b$ from $f(a)\neq f(b)$ , but also when we claim that the four cases 1–4 are exhaustive. In the presence of the Axiom of Extensionality, an operation on sets is a transformation that need not preserve extensional equivalence. Bell [7, 8] studies variations of both the Goodman–Myhill proof and Diaconescu’s proof in a set theory without extensionality.

The role of extensionality in the Goodman–Myhill proof becomes especially clear in an intensional framework such as Martin-Löf’s intuitionistic type theory, where a form of AC is a theorem, but where the addition of any of a number of extensionality principles—including what is there called extensional AC—yields LEM. We shall return to this in Section 7.

5 Notions of set

Here, we present, at least in brief, four influential constructive and intuitionistic notions of set: axiomatic, Brouwer’s original, Bishop’s, and Kleene–Kreisel–Troelstra. On all of these accounts, sets are suitably extensional entities. As we will show, none of these requires AC, even when they are coupled with apposite intuitionistic mathematics and commensurate understandings of the logical signs.

5.1 Axiomatic

There is a full range of axiomatic constructive and intuitionistic set theories, extending from the proof-theoretically weak, e.g., Harvey Friedman’s B, all the way to IZF, intuitionistic Zermelo–Fraenkel set theory, which is equiconsistent with full classical ZF. Each of these theories is inspired, in large part, by the familiar idiom and axioms of ZF. The first formalized and specifically intuitionistic set theory may have been Heyting’s [24]; more recent research was stimulated by Myhill’s ideas in [39]. All of them endeavor to capture a conception of set already on view, namely, that a set is a coin with two foundational sides. As a class, it is on the one side the extension of a mathematical predicate (perhaps with parameters); on the other side, as an object of set theory, its internal structure is a register of its locus, within a universe of sets, determined by the combinatorics of the membership relation.

Friedman’s [21] constructive set theory B was intended to formalize the constructive mathematics of Bishop within sets of finite rank over $\mathbb {N}$ . With its restricted forms of induction over the natural numbers, separation, replacement, and exponentiation (the latter standing in for the familiar powerset axiom), B is relatively weak proof-theoretically. Beeson [5, 6] shows that B is conservative over Heyting Arithmetic, HA. It features a restricted form of AC—with $\mathbb {N}$ a base—as an axiom. However, without such an axiom, no general form of AC is derivable in the reduced B, since the latter is a subtheory of classical ZF.

The intuitionistic small set theory SST in [38] has as its standard model the collection of pure cumulative sets of finite rank. It is definitionally equivalent to HA. In SST, AC is a theorem, but this is because the intended objects of the theory are all finite and decidable.

Aczel’s [1] contains axioms for CZF, a constructive version of Zermelo–Fraenkel set theory, as well as an interpretation of CZF in Martin-Löf’s intuitionistic type theory (see Section 7). Although CZF is consistent with the statement that $\mathbb {N}$ is a base, it does not derive it.

We shall need the following special case of AC, called $\mathbf {AC}_{\mathbb {N}, \mathbb {N}}$ :

$$\begin{align*}\forall x \in \mathbb{N} \ \exists y\in \mathbb{N} \ R(x,y) \ \rightarrow \ \exists f \in (\mathbb{N}\Rightarrow \mathbb{N})\ \forall x\in\mathbb{N} \ R(x,f(x)).\end{align*}$$

The strongest of the set theories listed above is IZF. It is relatively consistent with the invalidity of LEM [23], with Brouwer’s Theorem [20], and with intuitionistic Church’s Thesis [37]. As a subtheory of classical ZF, IZF fails to derive AC, and even $\mathbf {AC}_{\mathbb {N}, \mathbb {N}}$ . In IZF, as well as in its subtheories CZF and B, it is consistent that AC $_{\mathbb {N}, \mathbb {N}}$ fails. The Goodman–Myhill proof can be carried out in IZF, but not in its full generality in CZF and B, which feature restricted, rather than full, separation. Since both of these contain pairing as an axiom, however, the proof that $\{ a, b\}$ is a base just in case identity on it is decidable can be carried out in either system.

5.2 Brouwer’s original

Brouwer published repeatedly on an intuitionistic set theory, e.g., [12], but never offered, in his published works at least, a full axiomatic treatment of sets. He did, however, describe at least two concepts of sets or set-like collections: species in general and species arising from spreads. Neither of these demonstrates, or even suggests, that AC should be true.

First, a Brouwerian species is the extension of an extensional mathematical predicate, provided that the predicate does not employ any impredicative specification. Species are to be individuated extensionally, in the sense that species with the same members are the same:

Two species are said to be equal, or identical, if for each element of either of them, an element of the other equal to it can be indicated. [14, p. 9]

Moreover, elementhood in a species is to be extensional, in the sense that if a belongs to species S and $a = b$ , then b belongs to S, too:

properties supposable for mathematical entities previously acquired, satisfying the condition that if they hold for a certain mathematical entity, they also hold for all mathematical entities that have been defined to be ‘equal’ to it. [14, p. 8]

Brouwer explicitly allowed there to be species of higher type—species whose members are other species.

Brouwerian spreads are trees of sequences. In particular, a spread T is an inhabited, decidable collection of finite sequences of natural numbers satisfying two conditions:

1. 1. It is closed under predecessor: if a sequence s belongs to T, then so does every initial subsequence t of s.

2. 2. Each sequence s in T has at least one immediate successor: if $s \in T$ , then there is at least one sequence $t\in T$ extending s by a single component.

The species of members of a spread T consists of all the sequences each of whose initial segments belongs to T.⁴

Both these conceptions—species and spread—can be elaborated and developed theoretically ad infinitum, without lending any support either to AC in general or even to AC $_{\mathbb {N}, \mathbb {N}}$ . For instance, an intuitionistic theory of species satisfying full comprehension can be constructed over any model of the intuitionistic set theory IZF and then proven to be independent of AC for any sets and classes in the conjoint universe. Were AC assumed to hold for classes, it would also hold for sets and, by the Goodman–Myhill proof, would imply LEM.

5.3 Bishop

Bishop adopted a distinctively constructivist concept of set, writing,

The totality of all mathematical objects constructed in accord with certain requirements is called a set $\ldots $ Each set A will be endowed with a relation $=$ of equality. This relation is a matter of convention, except that it must be an equivalence relation. [9, p. 13]

Bishop elaborated on the conception—with its double specification, one for membership and one for equality—several pages later:

[A] set is defined by describing what must be done to construct an element of the set, and what must be done to show that two elements of the set are equal. [9, p. 63]

Bridges and Vîţă, distinguished followers of Bishop, explain why, on this “double specification” notion of set, one should not expect AC to hold generally over sets.⁵ They use the subscripted sign $=_{X}$ to denote an equality allied with a set X.

[T]he hypothesis

$$\begin{align*}\forall x\in X\ \exists y \in Y\ (\langle x,y\rangle \in S)\end{align*}$$

of AC means that we have an algorithm that, applied to each element x of X and the data showing that x belongs to X, constructs an element y of Y and demonstrates that $\langle x,y\rangle \in S$ . This much is clear. However, there is no guarantee that the algorithm will respect the equality relation on X—in other words, that if $x =_{X} x'$ , and the algorithm constructs y and $y'$ in Y such that $\langle x, y\rangle \in S$ and $\langle x',y'\rangle \in S$ , then $x' =_{Y} y'$ . Indeed, we should expect that the computation of y might use data that are associated with properties intrinsic to x that do not apply intrinsically to $x'$ . [11, p. 17]

Bridges and Vîţă do allow that $\mathbb {N}$ is a base, but, in their mathematical work, that assumption features as a separate postulation and not as a direct or indirect consequence of Bishop’s conception of set itself. The assumption that $\mathbb {N}$ is a base is consistent with the background set theory, since it holds in the Kleene realizability universe for IZF.

Once again, the foregoing argument against AC depends upon a plain extensionality requirement: that functions on sets preserve identity.

5.4 Kleene–Kreisel–Troelstra

The concept of realizability, crucial to the current metatheoretic understanding of intuitionism at every level, originated in a brilliant paper by Kleene [28]. Kleene’s interpretation of the formulas of intuitionistic arithmetic associates those formulas with collections of natural numbers generally treated as codes or indices of Turing machines. The association is specified recursively by laying down conditions, retracing the structures of formulas, under which a natural number n realizes formula $\phi $ or, in symbols, $n \Vdash \phi $ . For instance, for the material implication, $n \Vdash (\phi \rightarrow \psi )$ just in case

$$\begin{align*}\forall m \ (\text{if }m \Vdash \phi, \text{ then } \{n\}(m) \text{ is defined and } \{n\}(m)\Vdash \psi),\end{align*}$$

that is, for any m that realizes the antecedent $\phi $ , the Turing machine n computing the function $\lambda x. \{ n\}(x)$ applies to m and outputs a realizer (or a realizability witness) for the consequent $\psi $ .

A premier way to extend Kleene’s original idea to set theory and higher-order systems is by working with a two-part concept of set introduced by Kreisel and Troelstra [29]. First, realizability sets are defined: a realizability set S is any set of pairs $\langle n, x\rangle $ wherein the n’s are natural numbers and the x’s are members of some set A. In other words, a realizability set is a subset of the Cartesian product $\mathbb {N} \times A$ . When $\langle n, x\rangle $ belongs to the realizability set S, we write

$$\begin{align*}n \Vdash x \in S.\end{align*}$$

Second, when it comes to quantification over all realizability sets, we say that

$$\begin{align*}n \Vdash \forall s \ \phi(s) \text{ if and only if } \forall s \ n\Vdash \phi(s).\end{align*}$$

In short, quantification over realizability sets exerts no effect—or, in the jargon, is “uniform”—over the realizability relation $\Vdash $ .

A formula $\phi $ of the set-theoretic language holds under realizability just in case $\exists n \ n \Vdash \phi $ . The entire set theory IZF is sound with respect to this concept of realizability for sets: provably within IZF, for all sentences $\phi $ in the language of set theory, if IZF $\ \vdash \phi $ , then $\exists n \ n\Vdash \phi $ . The law of excluded middle fails outright under the realizability interpretation:

$$\begin{align*}\exists n \ n \Vdash \neg \forall p \ (p \vee \neg p).\end{align*}$$

Consequently, by Goodman–Myhill, AC is false in the realizability interpretation of IZF.

6 Brouwer–Heyting–Kolmogorov

Scholars of the subject often refer to a Brouwer–Heyting–Kolmogorov, or BHK, explanation of the connectives and quantifiers of intuitionistic mathematics. Like most semantic treatments, it is compositional. Some investigators, such as Michael Dummett, seem to have maintained that the truth of a general choice principle follows directly from the clauses of the BHK explanation governing the quantifier combination $\forall \exists $ in the antecedent of AC (see Section 8).

Since the BHK explanation is informal, any conclusions drawn from its clauses regarding the validity of a rule or principle will depend on how those clauses are formulated. We begin with the formulation given by Troelstra and van Dalen [51, p. 9] in terms of abstract proofs of some sort. Here are the relevant clauses:

1. (1) A proof of $\forall x\ C(x)$ is a construction that transforms a proof of $a \in A$ (A being the intended range of the variable x) into a proof of $C(a)$ .

2. (2) A proof of $\exists x\ C(x)$ is given by providing an element $a \in A$ and a proof of $C(a)$ .

3. (3) A proof of $C \rightarrow D$ is a construction that permits us to transform any proof of C into a proof of D.

On this understanding of the BHK explanation, there is no short and simple argument to the conclusion that AC is valid. Consider the antecedent of an instance of AC,

$$\begin{align*}\forall x \in A\ \exists y \in B \ R(x,y).\end{align*}$$

According to clauses (1) and (2), any proof of such a statement must be a construction c that transforms each $a \in A$ and each proof p of $a \in A$ into the provision of a $b \in B$ and a proof of $R(a, b)$ .

By contrast, according to (2) and (3), a proof of the consequent of AC,

$$ \begin{align*}\exists f \in (A \Rightarrow B)\ \forall x \in A \ R(x, f(x)),\end{align*} $$

must provide a function f with domain A and co-domain B such that, for all $a \in A$ , $R(a, f(a))$ is proven. According to (3), such an f as well as a proof of $\forall x\in A \ R(x,f(x))$ must somehow arise from a hypothetical proof c of the antecedent. That it will not, however, in general do.

A proof c of the antecedent is a construction taking an object a together with a proof p of $a\in A$ into a proof of $\exists y\in B \ R(x,y)$ . Such a construction will not, in general, give rise to a function on A itself. We cannot simply forget about the second argument to c, since there may be two distinct proofs, $p_1$ and $p_2$ , of $a\in A$ . Nor will it do to choose a distinguished proof $q_A(a)$ of $a\in A$ in a uniform way, since such a q will itself be a choice function.

In short, under this reading of BHK, the antecedent of AC will yield a choice operation—a transformation that need not preserve identity—on A, but not, in general, a choice function.

On another reading of BHK, the clause for the universal quantifier has the construction operating directly on the members of the domain, and not on proofs thereof:

A proof of $\forall x\ C(x)$ is a construction that for any element $a\in A$ yields a proof of $C(a)$ .

The motivation for this reading is that the notion of elementhood should be simple enough not to require proof—at most it requires computation. For instance, no proof is required for us to see that $2+2$ is an element of $\mathbb {N}$ . It suffices to compute $2+2$ to successor form, $s(s(s(s(0))))$ , in order for us to see that it can be generated by continued application of the successor function beginning from 0 (whence it is an element of $\mathbb {N}$ according to the first two Peano axioms).

Under this reading of BHK—which thus does not require a so-called “second clause” proving elementhood⁶ —the argument above that a $\forall \exists $ quantifier combination guarantees at most a choice operation, but not a choice function, breaks down. We cannot yet infer, however, that BHK in this formulation validates AC, since we still have no guarantee that the construction c taking every $a\in A$ to a proof $c(a)$ of $C(a)$ is indeed a function. Again, over $\mathbb {N}$ we might be able to extract a function from c, namely by first evaluating any given $n\in \mathbb {N}$ to zero or successor form and then applying c to the latter. Since n has a unique zero or successor form, this procedure yields a function. Over $\mathbb {R}$ , by contrast, we should not expect to be able to extract a function in this way. The method described clearly presupposes that identity over the underlying domain is decidable, which is not the case with $\mathbb {R}$ . In general, therefore, also this formulation of BHK fails to justify AC for all domains that intuitionists are interested in.

In conclusion we may therefore say that the BHK explanation validates AC only to the extent that the construction that according to it serves as a proof of a universally quantified proposition is a function, and not merely an operation, on the domain of quantification.

7 Intuitionistic type theory

We now turn to Per Martin-Löf’s intuitionistic, or constructive, type theory, where an intensional version of AC is a theorem. A correspondending extensional version of AC can be formulated and seen not to be constructively valid. We end the section by considering Aczel’s Presentation Axiom, which may be regarded as an attempt to capture intensional AC inside an extensional set theory.

7.1 Intensional Axiom of Choice

Howard [27] indicated how the correspondence between propositions and types that would later be called the Curry–Howard correspondence yields a choice function from an assumed proof of $\forall x\in \mathbb {N} \ \exists y\in \mathbb {N} \ R(x,y)$ . The formal language studied by Howard was, however, not rich enough to provide for the definition of such a function. Only with the more thoroughgoing implementation of the Curry–Howard correspondence by Martin-Löf in [34] did a choice function become formally definable, and then not only over $\mathbb {N}$ , but over any quantificational domain of Martin-Löf’s type theory.

The Curry–Howard correspondence correlates notions of logic with notions of type theory. In particular, propositions are identified as types: proposition A is identified as the type of proofs of A. By a proof of a proposition A one then understands an object making A true and not an act by means of which one convinces oneself of the truth of A. It is natural to think of a proof in this sense as a truthmaker of A, as noted by Sundholm [45]. Indeed, that a proposition is true means, under the Curry–Howard correspondence, that it is inhabited as a type, that a proof of it exists.

Just as one can define a type by saying what it is to be an object of that type, so one can define a proposition by saying what it is to be a proof of that proposition. Explaining propositions in this way is, in effect, just what the BHK explanation does; hence one sees the close relationship between it and the Curry–Howard correspondence. Curry–Howard, however, adds precision by laying down how a (canonical) proof of a proposition is formed from its parts. In particular, a proof of an existential proposition, $\exists x\in A \ C(x)$ , is stipulated to be a pair $\langle a,p\rangle $ where a is an element of the domain of quantification, A, and p is a proof of $C(a)$ . A proof of a universal proposition, $\forall x\in A \ C(x)$ , is stipulated to be a lambda term, $\lambda x.p(x)$ , where $p(a)$ is a proof of $C(a)$ for every a in the domain of quantification, A.

When defining a type A in intuitionistic type theory, it is in fact not enough just to say what it is to be an object of type A. In addition, one must say what it is to be identical objects of type A. In a terminology sometimes used by philosophers: to define a type one must give both a criterion of application and a criterion of identity (cf. Bishop’s notion of set, Section 5.3). Every type therefore comes equipped at birth with a notion of identity, which is usually expressed in the form $a=b : A$ (this could be read as “a is the same A as b”). It then makes sense to speak of functions on types: a function, $f(x)$ , from A to B is a transformation such that $f(a)=f(b): B$ whenever $a=b : A$ . All open terms in intuitionistic type theory are functions in this sense. It follows that if $p(a)$ is a proof of $C(a)$ for every a in the domain of quantification, A, then $p(a)=p(b):C(a)$ whenever $a=b : A$ .

Under the Curry–Howard correspondence, the formation of $\lambda x.p(x)$ as a proof of $\forall x\in A \ C(x)$ corresponds to an application of the $\forall $ -introduction rule in natural deduction. Corresponding to an application of the $\forall $ -elimination rule is the formation of a term of the form $\mathbf {ap}(c,a)$ , whenever c is a proof of $\forall x\in A \ C(x)$ and a is an element of A. Whereas the $\lambda $ -operator is primitive, the $\mathbf {ap}$ -operator is defined, namely by the equation

$$\begin{align*}\mathbf{ap}(\lambda x.p(x), a) = p(a) : C(a).\end{align*}$$

Under the Curry–Howard correspondence, this equation corresponds to the $\forall $ -reduction rule of natural deduction introduced by Prawitz [41].

The BHK clauses for implication, $A\rightarrow B$ , and the universal quantifier, $\forall x\in A \ C(x)$ , both invoke the idea of a transformation, in the former case from A to B, in the latter case from any a in A to $C(a)$ . In intuitionistic type theory, implication comes out as a special case of universal quantification, namely the case where each $C(a)$ is one and the same proposition, B. In particular, the $\lambda $ -operator can be used to construct a proof, $\lambda x.p(x)$ , of $A\rightarrow B$ provided $p(a)$ is a proof of B whenever a is a proof of A.

In light of the $\mathbf {ap}$ -operator and the functionality of open terms, we may think of $\lambda x.p(x)$ as a function from A into the family of types (or propositions) $\{C(x)\}_{x\in A}$ . At the end of the previous section we noted that for the BHK explanation to justify AC, the construction that serves as a proof of a universally quantified proposition must be a function. This requirement is now met. To obtain a choice function from a proof of the antecedent, $\forall x\in A \ \exists y \in B \ R(x,y)$ , of AC, however, also projection functions are required.

Just as $\forall $ -elimination corresponds to the $\mathbf {ap}$ -operator, so $\exists $ -elimination corresponds to a certain operator. We shall not describe the precise workings of this operator here—suffice it to say that from it, one can define first and second projection functions,

$$\begin{align*}\mathbf{fst}(\langle a,b\rangle) = a\quad\quad\quad \mathbf{snd}(\langle a,b\rangle) = b.\end{align*}$$

Given a proof c of an existential proposition, $\exists x\in A \ C(x)$ , $\mathbf {fst}(c)$ is an element of the domain of quantification, A, and $\mathbf {snd}(c)$ is a proof of the proposition $C(\mathbf {fst}(c))$ . It was in specifying the type of $\mathbf {snd}(c)$ that Howard hit the limits of his formal system. One needs for that purpose to have access to the notion of a propositional function over the proofs of a proposition. In particular, one needs access to the propositional function $C(\mathbf {fst}(z))$ over proofs z of $\exists x\in A \ C(x)$ . This clearly requires a thoroughgoing implementation of the Curry–Howard correspondence.⁷

Suppose c is a proof of an instance of the antecedent of AC, that is, of a proposition $\forall x\in A \ \exists y\in B \ R(x,y)$ , and let a be an element of the domain A. Then $\mathbf {ap}(c,a)$ is a proof of $\exists y\in B \ R(a,y)$ . Using the two projection functions, we find

$$\begin{align*}\mathbf{snd}(\mathbf{ap}(c,a)) \in R(a, \mathbf{fst}(\mathbf{ap}(c,a))).\end{align*}$$

By means of the $\lambda $ -operator, we can then form a choice function

$$\begin{align*}\lambda x.\mathbf{fst}(\mathbf{ap}(c,x)) \in (A\Rightarrow B).\end{align*}$$

Given these ingredients, it is now an easy exercise to construct the full proof of AC (for details, see [35]). The proof goes through also if the co-domain of the choice function is a family of types, $B(x)$ , depending on the domain, A, or more precisely, if the choice function belongs to the generalized Cartesian product $\prod _{x\in A} B(x)$ . This more general form of the Axiom of Choice includes, as a special case, the formulation that the Cartesian product of a family of non-empty types is non-empty.

Any type that may serve as the domain of the universal quantifier in intuitionistic type theory is therefore a base. Included among these are $\mathbb {N}$ as well as any type that can be formed from $\mathbb {N}$ by means of product, disjoint union and exponentiation, such as $\mathbb {N}\times \mathbb {N}$ , $\mathbb {N}\Rightarrow \mathbb {N}$ , and $(\mathbb {N}\Rightarrow \mathbb {N})\Rightarrow \mathbb {N}$ . The domain $\mathbb {R}$ of real numbers, however, remains out of reach. A domain Cauchy of Cauchy sequences of fractions can be defined as a type (the canonical elements of this type will be pairs $\langle s,p\rangle $ , where s is a sequence of fractions and p is a proof that s is Cauchy). The construction needed to obtain $\mathbb {R}$ from Cauchy, however, is not among the type-forming operations of (standard) intuitionistic type theory.

We obtain the domain $\mathbb {R}$ from Cauchy by, in effect, identifying certain Cauchy sequences that are not identical according to the identity relation native to the type Cauchy. A standard way of implementing this construction is by the formation of a quotient structure. Another way is to let co-convergence simulate identity on Cauchy. The type Cauchy will continue to have its native identity relation, but we require that all functions defined on Cauchy must respect co-convergence, so that co-convergence in effect plays the role of identity on Cauchy. Martin-Löf follows the latter course in clarifying why there is no contradiction between the provability of AC in his system and results such as Diaconescu’s Theorem.⁸

7.2 Extensional Axiom of Choice

It may be difficult to pin down in the abstract just what extensionality amounts to, beyond a certain family resemblance among certain principles. In intuitionistic type theory it is natural to say that an extensionality principle is a principle that identifies elements of a type A that are not identical according to the identity relation native to A. Likewise, an extensional construct is a construct that renders elements of A identical that are not identical according to the identity relation native to A.

Function extensionality, according to which $\lambda x.p(x)$ and $\lambda x.q(x)$ are identical elements of $A\Rightarrow B$ if and only if $p(a)$ and $q(a)$ are identical for every $a\in A$ , is one example of an extensionality principle. Another example is the principle according to which propositions are identical if and only if they are materially equivalent. The type $\mathbb {R}$ , regarded as the type Cauchy equipped with co-convergence as the identity relation is an extensional construct, and so is Aczel’s constructive version of the cumulative hierarchy of sets serving as a model of CZF [1–3]. The model consists of a type V together with a relation $\sim _{\mathbf {V}}$ of extensional equality. From the definition of V, it is clear that it contains infinitely many empty sets. The relation $\sim _{\mathbf {V}}$ identifies all of these and, more generally, any two sets a and b such that $\forall x \in a \ \exists y \in b \,(x\sim _{\mathbf {V}} y)$ and $\forall y \in b \ \exists x\in a \,(x\sim _{\mathbf {V}} y)$ .

In light of this understanding of extensionality, we see that it was natural for Martin-Löf to call an extensional set a type A equipped with an equivalence relation that is to simulate identity on A.⁹ Where $\sim $ is the equivalence relation in question, the extensional set may be written as the pair $(A,\sim )$ . Sets in the sense of set theory are extensional, not only in the sense that the set-theoretical Axiom of Extensionality holds for them, but also in the sense that extensional constructs, such as quotient formation and naive separation,¹⁰ preserve sethood.

With the notion of extensional set in hand, we can formulate the extensional axiom of choice, ExtAC, which requires that the choice function respects the equivalence relations $\sim _A$ and $\sim _B$ simulating identity on A and B:

$$\begin{align*}\forall x\in A \ \exists y\in B \ R(x,y) \ \rightarrow \ \exists f : \big((A,\sim_A) \Rightarrow (B,\sim_B)\big) \ \forall x\in A \ R(x,f(x)).\end{align*}$$

By the notation $f : \big ((A,\sim _A)\Rightarrow (B,\sim _B)\big )$ we mean that f is a function from A to B that respects the equivalence relations $\sim _A$ and $\sim _B$ in the sense that $\forall x,y \in A \ (x\sim _A y\rightarrow f(x)\sim _B f(y))$ is true. Since we are in the setting of extensional sets, it is natural to require that R be an extensional relation, that is, that $R(x,y)$ and $R(x',y')$ be materially equivalent whenever $x\sim _A x'$ and $y\sim _B y'$ hold.

As Martin-Löf [36] makes clear, it is ExtAC that corresponds in intuitionistic type theory to the Axiom of Choice in set theory. Apart from the conceptual argument that a set in the sense of set theory is better understood as an extensional set $(A, \sim )$ than as a type A, there is also a compelling technical argument: when ExtAC is assumed, Aczel’s model V validates (set-theoretical) AC.

The constructive unacceptability of ExtAC is borne out by Carlström [15], who shows that, in intuitionistic type theory, it entails the Law of Excluded Middle.¹¹ Indeed, we have no reason to expect that the choice function constructed from a proof of $\forall x\in A \ \exists y\in B \ R(x,y)$ is extensional in the sense required by ExtAC. That extensionality is the culprit here is nicely illustrated by the fact that ExtAC is just one of many extensionality principles which when added to intuitionistic type theory yields classical logic [30, 32, 52].

Although ExtAC is constructively unacceptable, it is a theorem of intuitionistic type theory that a choice operation always exists: this is just what intensional AC becomes in the setting of extensional sets. An operation, O, between extensional sets $(A,\sim _A)$ and $(B,\sim _B)$ is here simply a function from A to B: it respects the identity relations native to A and B, but need not respect the equivalence relations $\sim _A$ and $\sim _B$ .

7.3 The Presentation Axiom

On each type, A, there is a binary propositional function of identity, $=_A$ , defined as the smallest reflexive relation on A. In the setting of extensional sets, where an arbitrary equivalence relation on A may serve as identity, we may call the relation $=_A$ the true identity relation on A. Let us call an extensional set of the form $(A,=_A)$ an intensional-extensional set. All intensional–extensional sets are bases. Moreover, any extensional set $(A,\sim )$ is the surjective image of an intensional–extensional set, namely the image of $(A,=_A)$ under the identity function on A. (If $(A,\sim )$ is regarded as a quotient structure, then the map in question is the natural one.) Extensional sets known to be bases—the intensional–extensional sets—thus form a subdomain of all extensional sets, and every extensional set is the surjective image of an extensional set from this subdomain.

Abstracting this situation from the type-theoretical framework, we arrive at the so-called Presentation Axiom, PAx: every set is the surjective image of a base.¹² The axiom holds in Aczel’s V, and hence it is consistent with CZF and, moreover, constructively acceptable. It is not, however, a theorem of CZF. Indeed, it is not even a theorem of classical ZF plus the axiom of dependent choices [42]. Aczel’s proof [2] shows, more concretely, that, in V, (i) sets formed by means of set-theoretical correlates of the standard type-forming operations of intuitionistic type theory are all bases and (ii) every set is the surjective image of such a set. The proof thus gives expression to the idea that the quantificational domains of type theory—all of which are bases—form a subdomain of all sets, some of which fail to be bases.

8 Dummett

We cannot, with utter certainty, lay a finger on the ultimate origin of the thought that intuitionists are somehow obliged to accept a general form of AC, but Dummett [18] has been especially influential, at least among philosophers, and certain passages in that work pertaining to AC are at least misleading in their phrasing. Here is one of them.

It might at first seem surprising that in a system of constructive mathematics we should adopt as an axiom the Axiom of Choice, which has been looked at askance on constructive grounds. The fact is, however, that the axiom is only dubious under a half-hearted platonistic interpretation of the quantifiers. [18, p. 52]

We will not take up the question whether there is such a thing as a platonistic interpretation of the quantifiers, of which, presumably, classical mathematicians are guilty. Dummett’s language here seems to suggest that intuitionists accept AC generally, “when we interpret the quantifiers intuitionistically.”

What follows the passage just cited is a sketch of an argument to the conclusion that, in our terms, the collection $\mathbb {N}$ of natural numbers is a base, not that AC holds generally:

[T]he antecedent of AC $_{n,m}$ [our AC $_{\mathbb {N}, \mathbb {N}}$ ] expresses not merely that for each n we can effectively find an m for which we can prove $A(n,m)$ , but that we have a single effective procedure which we can recognize as yielding, for each n, such an m: the consequent merely makes this explicit, the constructive function $\ldots $ being that which, when applied to n gives a suitable m. [18, p. 53]

As we have explained in Section 5 and 6, the truth of AC on an intuitionistic vision is nowise obvious a priori, even on some BHK-style interpretations of the quantifiers. Furthermore, it is not an understanding of quantifiers alone that might require the truth of AC, but, at best, only an understanding of quantifiers together with an account of sets generally.

Dummett does construe the quantifiers, when ranging over natural numbers, in a way roughly in accord with the BHK explanation, but he never seems to say much about what that explanation would yield when the quantifiers are meant to range over arbitrary sets or species of numbers—which he allows do exist.

In particular, Dummett (ibid., p. 39) demands that there be a full hierarchy of species, generated by predicative comprehension at each level. Therefore, he would have to allow that, for any species $S_{1}$ and $S_{2}$ of the same level $\alpha $ in the hierarchy, there is an unordered pair species $\{ S_{1}, S_{2} \}$ of level $\alpha + 1$ , since unordered pairs are specifiable predicatively. This conception of species would then be open to the Goodman–Myhill argument of Section 4. So, if Dummett insists upon full AC, he must also hold that, within any level, identity over all species of that level is decidable. Furthermore, according to Dummett (ibid., p. 39), “a real number is a species”; consequently, among the real numbers of any given level, $\{ 0\}$ would be decidable. ¹³

Finally, if there is a species of all real numbers, Dummett appears to have no ready defense against the argument of Section 3, since it is so easy to prove that every real number is majorized by some natural number. Again, from AC, it follows that there are discontinuous functions.

Dummett takes up the issue of AC once again when introducing $\mathbb {N} \Rightarrow \mathbb {N}$ —conceived by him as a collection of Brouwerian choice sequences:

In particular, we may consider a statement of the form

$$ \begin{align*}\forall \alpha\exists n. \ B(\alpha, n),\end{align*} $$

where $B(\alpha , n)$ is extensional [and $\alpha $ ranges over choice sequences]. As always, a form of Axiom of Choice holds good: the statement involves that there must be a uniform effective procedure for finding, for each given $\alpha $ , an n such that $B(\alpha , n)$ . [18, p. 64]

It is not merely to the flippant “as always, a form of Axiom of Choice holds good” that we object. There is little or no reason here, in talking of sequences, to think that the “effective procedure for finding” amounts to a function on real numbers, rather than an operation—especially in view of the fact that, in general, choice sequences are often presented intensionally, in terms of descriptions or rules, rather than extensionally (see, e.g., [50]).

A consistent defender of Dummett cannot here rescue him by “going operational” and claiming that the “uniform effective procedure” that arises from the interpretation of the antecedent of AC was really meant by him to be an operation rather than a function. Dummett refers to the effective method he thinks to underlie the antecedent of AC as yielding

[a] constructive function a being that which, when applied to n, gives a suitable $m \ldots $ the variables $a \ldots $ being taken to range over constructive (effectively calculable) functions of natural numbers. Unary constructive functions of natural numbers may be identified with lawlike sequences of natural numbers. [18, p. 53]

In a lecture from 1992 that has only recently been published [19], Dummett qualifies his previous apparently unconditional acceptance of AC:

Bishop’s remark that the validity of the axiom of choice is “implied in the very meaning of existence”, as constructively understood, has in some sense to be true; but it is true generally only if the identity relation on the domain of the choice function is strict (i.e. intensional). [19, p. 496]

From the context it appears that it was the Goodman–Myhill argument that had forced Dummett to rethink his stance. For finitely presented objects, such as the natural numbers, AC is unproblematic. A natural number evaluates to a unique zero or successor form; hence we can extract a function from a construction c witnessing the truth of a universally quantified proposition by considering its values on these canonical forms, i.e., $c(0)$ , $c(0')$ , $c(0")$ , etc. This method is, according to Dummett, no longer available for infinitely presented objects; hence for a domain A of such objects, AC will be validated by a BHK-like semantics only if identity on A is “strict (i.e., intensional).” Dummett admits that species may be intensional, but he argues at length that real numbers and infinite sequences are not. He thus accepts, albeit only implicitly, that AC fails for $\mathbb {R}$ and for domains of infinite sequences.

9 Some formal theories, Church’s thesis, and AC

There are far too many intuitionistic formal theories of numbers, functions, sets, and types for us to attempt a full survey here of their respective deductive relations with prominent forms of AC. Even so, we would like to remark on the standing of AC and formalized Church’s Thesis (CT—see definition below) within three of the theories better known to logicians and philosophers who are not specialists in this subject.

Definition.

1. 1. A formal theory T is constructively consistent just in case T does not derive the validity of LEM—when that validity is standardly expressed in the language of T.¹⁴

2. 2. Let T be Kleene’s computation predicate and U his upshot function, taking the code of a complete computation and returning the output thereof. The following principle is called intuitionistic Church’s Thesis, Church’s Thesis, or CT for short:

   (CT) $$\begin{align} \forall n \exists m \ A(n,m) \ \rightarrow \ \exists e \forall n \exists p \exists m \ \big(T(e, n, p) \wedge U(p, m) \wedge A(n,m)\big).\end{align}$$

The principle CT is clearly recognizable as an effective form of $\mathbf {AC}_{\mathbb {N}, \mathbb {N}}$ . It says, in effect, that for every binary relation $A(n,m)$ on $\mathbb {N}$ satisfying $\forall n\exists m \ A(n,m)$ , a Turing computable choice function exists.

First-order Heyting Arithmetic, or HA, formalized with the axioms of Peano Arithmetic within intuitionistic predicate logic, has no variables for (unencoded) sets. Kleene’s realizability shows that HA is constructively consistent with CT, written as a first-order scheme, as well as with certain generalizations of CT [51, pp. 195–203].

Second-order Heyting Arithmetic, or HAS, formalized with the axioms of second-order Peano Arithmetic within second-order intuitionistic predicate logic, features variables for sets of numbers explicitly. Kleene–Kreisel–Troelstra realizability shows that HAS is constructively consistent with CT, as well as with second-order generalizations of it [49, pp. 203–204]. Every finite set is provably a base, but $\mathbb {N}$ cannot be shown to be a base in HAS.

In the intuitionistic Zermelo–Fraenkel set theory IZF, every finite set is provably a base. The set of natural numbers, $\mathbb {N}$ , is not provably a base, but it is constructively consistent with IZF to assume that it is. Church’s thesis and various set-theoretic generalizations thereof are constructively consistent, but—as we have seen repeatedly—full AC itself is not constructively consistent with IZF.

10 Conclusion

To dispel any illusion that an unrestricted AC holds generally for intuitionists, readers are advised to keep in mind the relevant differences between:

• • sets and types,

• • extensional and intensional contexts, and

• • functions and operations.

As understood here, AC concerns (extensional) sets and functions defined on them. Sets in this sense are individuated by an axiom of extensionality and admit of extensional constructs such as quotients and naive separation (see footnote 10 for an explanation of this notion). A function on such sets preserves equality—unlike an operation, which need not preserve equality. In the consequent of AC,

$$\begin{align*}\exists f \in (A \Rightarrow B) \ \forall a \in A \ R(a, f(a)).\end{align*}$$

A and B are (extensional) sets, and f ranges over functions on such sets. If A and B are types instead, and objects are individuated intensionally, as in intuitionistic type theory, then a version of AC holds, but this intensional AC must be distinguished from the extensional AC. When transported to an extensional setting, intensional AC guarantees the existence of a choice operation, but not the existence of a choice function.

Unless a set theory is tightly constrained, say with respect to the Axiom of Separation, as in, for example, Friedman’s B, Aczel’s CZF of the small set theory in [38], AC will not hold over entire universes of sets intuitionistically. Some sets may be assumed to be bases. The universe may look, for instance, as set out in the Presentation Axiom, $\mathbf {PAx}$ , according to which each set is the surjective image of a base.

The logical situation within intuitionistic mathematics of general, extensional AC is broadly analogous to that of LEM. Proofs such as that of Brouwer’s Continuity Theorem demonstrate that LEM fails in general: it is false that, for any statement $\phi $ , $\phi $ either holds or it does not. That said, LEM (or restricted versions of it) might be seen to hold locally, for one (mathematical) reason or another. For instance, identity for natural and for rational numbers satisfy LEM, while identity for real numbers does not. As we have seen, within intuitionistic real analysis and set theory, AC cannot hold in general, but some particular sets or other, such as $\mathbb {N}$ , could be bases. One could say that, intuitionistically, AC sometimes holds locally, but it cannot hold globally.