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 = BA
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 Cx:A Φ(x) of the Φ(x)'s.
To translate all this into the language of CDTT[4], one uses the following concordance:
Logical Operation Set-Theoretic Operation Type-Theoretic Operation ∧ × × ∨ + two-term dependent sum → set exponentiation type exponentiation ∀x cartesian product ∏i ∈ I dependent product ∏x:A ∃x coproduct or disjoint union Ci ∈ 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:BA∀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 BA 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:BA ∀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∃yR(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:ACy:B Φ(x, y)) and Cf:BA ∏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 Mij ↔ ∃f ∈ JI ∀i ∈ I Mif(i)
where <Mij: 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 ∈ ICj ∈ J Mij and Cf ∈ JI ∏i ∈ I Mif(i). On the other hand, AC interpreted set-theoretically can be presented in the form of the distributive law
(**) ∩i ∈ I∪j ∈ J Mij = ∪f ∈ JI ∩i ∈ I Mif(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 Ci ∈ 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 Mi (with each Mi a singleton) now becomes [Ci ∈ 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 Mij is interpreted as the singleton
(1) ∏i ∈ I[Cj∈ J Mij]
and the proposition ∃f ∈ JI ∀i ∈ I Mif(i) as the singleton
(2) [Cf ∈ JI ∏i ∈ I Mif(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 Mij is nonempty. But to give an element of (2) amounts to specifying maps f ∈ JI and g with domain I such that ∀i ∈ I g(i) ∈ Mif(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.