#### Supplement to The Axiom of Choice

## The Axiom of Choice in Type Theory

In conclusion, we examine the role of the Axiom of Choice in type
theory. The type theory we consider here is the *constructive
dependent type theory* (**CDTT)**
introduced^{[1]}
by Per Martin-Löf (1975, 1982, 1984) . This theory is both
predicative (so that in particular it lacks a type of propositions),
and based on intuitionistic
logic^{[2]}.
Also, as its name indicates, it contains *dependent* types,
wherein types can depend on, or “vary over” other
types. Type symbols may accordingly take the form
**B**(*x*), with *x* a variable of a given
type **A**: **B**(*x*) is then a type
dependent on or varying over the type **A**. It is
through the presence of dependent types that *AC* becomes
expressible in **CDTT**.

**CDTT** embodies the so-called *propositions-as-
types* doctrine, the central thesis of which is that each
proposition is to be *identified* with the type, set, or
assemblage of its
proofs^{[3]}.
As a result, such proof types, or sets of proofs, have to be
accounted the *only* types, or sets. Strikingly, then, in the
propositions-as-types doctrine, a type, or set, simply *is* the
type, or set, of proofs of a proposition, and, reciprocally, a
proposition *is* just the type, or set, of its proofs.

It turns out that **ACL**, the “logical”
form of the axiom of choice, is not merely formulable in
**CDTT**, *but actually derivable* in it. To see
this, we need to outline the correspondence between logical operators
and operations on types in **CDTT** obtained by
implementing the “propositions-as-types” doctrine. This is
most simply done by sketching Tait's [1994] exposition of the idea in
set-theoretic terms. To begin with, consider two
propositions/types/sets **A** and
**B**. What should be required of a proof
*f* of, for example, the implication **A** →
**B**? Just that, given any proof *x* of
**A**, *f* should yield a proof of
**B**, that is, *f* should be a function from
**A** to **B**. In other words, the
proposition **A** **→**
**B** is just the type of functions from
**A** to **B**:

A→B=B^{A}

Similarly, all that should be required of a proof *c* of the
conjunction **A** ∧ **B** is that it
should yield proofs *x* and *y* of **A**
and **B**, respectively. From this point of view
**A** ∧ **B** is accordingly just the
type **A** × **B** of all pairs
(*x*, *y*), with *x* of type **A**
(we write this as *x*: **A)** and *y*:
**B**.

A proof of the disjunction **A** ∨ **B**
is either a proof of **A** or a proof of
**B** together with the information as to which of
**A** or **B** it is a proof. That is, if we
introduce the type **2** with the two distinct elements 0
and 1, a proof of **A** ∨ **B** may be
identified as a pair (*c*, *n*) in which either
*c* is a proof of **A** and *n* is 0, or
*c* is a proof of **B** and *n* is 1. This
means that **A** ∨ **B** should be
construed as the disjoint union **A** +
**B** of **A** and **B**.

The true proposition **T** may be identified with the
one element type **1** = {0}: 0 thus counts as the unique
proof of **T**. The false proposition ⊥ is taken to
be a proposition which lacks a proof altogether: accordingly ⊥ is
identified with the empty set ∅. The negation
¬**A** of a proposition **A** is defined
as **A** → ⊥, which therefore becomes
identified with the set **A**^{∅}.

A proposition *A* is deemed to be true if it (i.e, the
associated type **A**) has an element, that is, if there
is a function **1** **→**
**A**. Accordingly the *law of excluded middle*
for a proposition *A* becomes the assertion that there is a
function **1** → A + ∅^{A}.

In order to deal with the quantifiers we require operations defined
on families of types, that is, types
**Φ**(*x*) depending on objects *x* of
some type **A**. By analogy with the case **A
→ B**, a proof *f* of the proposition
∀*x*:**A**
**Φ**(*x*), that is, an object of type
∀*x*:**A**
**Φ**(*x*), should associate with each
*x*:**A** a proof of
**Φ**(*x*). So *f* is just a function
with domain *A* such that, for each
*x*:**A**, *fx* is of type
**Φ**(*x*). That is,
∀*x*:**A**
**Φ**(*x*) is the *product*
Π*x*:**A** **Φ**(*x*)
of the **Φ**(*x*)'s. We use the
λ-notation in writing *f* as λ*xfx*.

A proof of the proposition ∃*x*:**A**
**Φ**(*x*), that is, an object of type
∃*x*:**A**
**Φ**(*x*), should determine an object
*x*:**A** and a proof *y* of
**Φ**(*x*), and *vice-versa*. So a
proof of this proposition is just a pair (*x*, *y*) with
*x*:**A** and
*y*:**Φ**(*x*). Therefore
∃*x*:**A**
**Φ**(*x*) is the *disjoint union*, or
*coproduct* *C**x*:**A**
**Φ**(*x*) of the
**Φ**(*x*)'s.

To translate all this into the language of
**CDTT**^{[4]},
one uses the following concordance:

LogicalOperation |
Set-TheoreticOperation |
Type-TheoreticOperation |

∧ | × | × |

∨ | + | two-term dependent sum |

→ | set exponentiation | type exponentiation |

∀x |
cartesian product ∏_{i ∈ I} |
dependent product ∏x:A |

∃x |
coproduct or disjoint union C_{i ∈ I} |
dependent sum Cx:A |

In **CDTT** the logical version **ACL** of
*AC* takes the form of the proposition

ACLT:

∀x:A∃y:BΦ(x,y)) → ∃f:B^{A}∀x:AΦ(x,fx)).

Now **ACLT** is *provable* in
**CDTT**, as the following argument shows. To begin with,
again following Tait, we introduce the functions σ, π,
π′ of types
∀*x*:**A**(**Φ**(*x*)
→ ∃*x*:**A**
**Φ**(*x*)),
∃*x*:**A**φ(*x*) →
**A**, and ∀*y*:
(∃*x***Φ**(*x*)).**Φ**(π(*y*))
as follows. If *b*:**A** and *c*:
**Φ**(*b*), then σ*bc * is
(*b*, *c*). If *d*:
∃*x*:**A**
**Φ**(*x*), then *d* is of the form
(*b*, *c*) and in that case π(*d*) =
*b* and π′(*d*) = *c*. These yield the
equations

π(σ bc) =bπ′(σ bc) =cσ(π d)(π′d) =d.

Now let *u* be a proof of the antecedent
∀*x*:**A**∃*y*:**B**
**Φ**(*x*, *y*)) of
**ACLT.** Then, for any *x*: **A**,
π(*ux*) is of type **B** and
π′(*ux*) is a proof of
**Φ**(*x*, π*ux*). So
*s*(*u*) = λ*x*π(*ux*) is of
type **B**^{A} and
*t*(*u*) = λ*x*π′(*ux*) is
a proof of ∀*x*:**A**
**Φ**(*x*,
*s*(*u*)*x*). Accordingly
λ*u*σ*s*(*u*)*t*(*u*)
is a proof of
∀*x*:**A**∃*y*:**B**
**Φ**(*x*, *y*)) →
∃*x*:**B**^{A}
∀*x*:**A****Φ**(*x*,
*fx*)), so that **ACLT** is derivable in
**CDTT**.

Put informally, what this shows is that in **CDTT** the
consequent of **ACLT** means *nothing more than its
antecedent*. Indeed, in many versions of constructive mathematics
the assertability of an alternation of quantifiers
∀*x*∃*y**R*(*x*,*y*)
means *precisely* that one is given a function *f* for
which *R*(*x*,*fx*) holds for all *x*.

We note that in ordinary set theory the argument establishes the
*isomorphism* of the sets
∏*x*:**A***C**y*:**B
Φ**(*x*, *y*)) and
*C**f*:**B**^{A}
∏*x*:**A** **Φ**(*x*,
*fx*)), but *not* the validity of the usual axiom of
choice. This is because in set theory **AC** is not
represented by this isomorphism, but rather by the equality —
the set-theoretic
distributive law^{[5]}
obtained by replacing ∏ by ∩ and *C* by ∪, namely

∩_{x ∈ A}∪_{y ∈ B}Φ(x,y) = ∪_{f ∈ BA}∩_{x ∈ A}Φ(x,fx)

While in **CDTT** *AC* is provable, and so *a
fortiori* has no “untoward” logical consequences, in
intuitionistic set theory this is far from being the case, for, as we
have noted, in the latter *AC* implies the law of excluded
middle. In other words, *AC* interpreted à la
propositions-as-types is
tautologous^{[6]},
yet construed set-theoretically it is anything but, since so
construed its affirmation yields classical logic. This prompts the
question: what modification needs to be made to the
propositions-as-types doctrine so as to yield the set-theoretic
interpretation of *AC*? An illuminating answer has been given
by Maietti (2005) through the use of so-called *monotypes* (or
mono-objects), that is, (dependent) types containing at most one
entity or having at most one proof. In set theory, mono-objects are
*singletons*, that is, sets containing at most one
element^{[7]}.

Maietti's modification of the propositions-as-types doctrine to
bring it into line with the set-theoretic interpretation of formulas
is, in essence, to take propositions (or formulas) to correspond to
*mono*-objects, that is, singletons, rather than to
*arbitrary* sets. Let us call this the
*propositions-as-monotypes* interpretation.

Now, finally, let us reconsider *AC* under the
propositions-as-monotypes interpretation within set
theory**. ** It will be convenient to rephrase
*AC* as the assertion

(*) ∀ i∈I∃j∈J M_{ij}↔ ∃f∈J^{I}∀i∈I M_{if(i)}

where <*M*_{ij}: *i* ∈
*I*, *j* ∈ *J*> is any doubly indexed
family of propositions (or sets). In the “propositions as
types” interpretation, (*) corresponds, as we know, to the
existence of an isomorphism between ∏_{i ∈
I}*C*_{j ∈ J}
*M*_{ij} and *C*_{f ∈
JI} ∏_{i ∈
I} *M*_{if(i)}. On the other
hand, *AC* interpreted set-theoretically can be presented in
the form of the distributive law

(**) ∩ _{i ∈ I}∪_{j ∈ J}M_{ij}= ∪_{f ∈ JI}∩_{i ∈ I}M_{if(i)}.

In the propositions-as-types interpretation, the universal quantifier
∀*i* ∈ *I* corresponds to the product
∏_{i ∈ I} and the existential
quantifier ∃*i* ∈ *I* to the coproduct
*C*_{i ∈ I}. Now in the
propositions-as-monotypes interpretation, wherein formulas correspond
to singletons, ∀*i* ∈ *I* continues to
correspond to ∏_{i ∈ I}, since the
product of singletons is still a singleton. But the interpretation of
∃*i* ∈ *I* is *changed*. In fact, the
interpretation of ∃*i* ∈ *I*
*M*_{i} (with each
*M*_{i} a singleton) now becomes
[*C*_{i ∈ I}], where for each
set *X*, [*X*] = {*u*: *u* = 0 ∧
∃*x*. *x* ∈ *X*} is the *canonical
singleton* associated with *X*. Thinking of *X* as a
set, the singleton [*X*] reflects the nonemptiness of
*X* in that *X* has an element if and only if
[*X*] has 0 as its unique element. Thinking of *X* as a
proposition, the proposition [*X*] reflects the provability of
*X* in that *X* has a proof if and only if the
proposition [*X*] has 0 as its unique proof.

It follows that, under the propositions-as-monotypes interpretation,
the proposition ∀*i* ∈ *I* ∃*j*
∈ *J* *M*_{ij} is interpreted as
the singleton

(1) ∏ _{i ∈ I}[C_{j∈ J }M_{ij}]

and the proposition ∃*f* ∈
*J*^{I} ∀*i* ∈ *I*
*M*_{if(i)} as the singleton

(2) [ C_{f ∈ JI}∏_{i ∈ I}M_{if(i)}]

Under the propositions-as-monotypes interpretation *AC* would
be construed as asserting the existence of an isomorphism between (1)
and (2).

Now it is readily seen that to give an element of (1) amounts to no
more than affirming that, for every *i* ∈ *I*,
∪_{j ∈ J}
*M*_{ij} is nonempty. But to give an element
of (2) amounts to specifying maps *f* ∈
*J*^{I} and *g* with domain *I*
such that ∀*i* ∈ *I* *g*(*i*)
∈ *M*_{if(i)}. It follows that to assert
the existence of an isomorphism between (1) and (2), that is, to
assert *AC* under the propositions-as-monotypes interpretation,
is tantamount to asserting *AC* in the form (**), which in turn
yields **ACL** and so the Law of Excluded Middle. This is
in sharp contrast with *AC* under the propositions-as-types
interpretation, where, as we have seen, its assertion is automatically
correct and so has no nonconstructive consequences.