In slide 28 of these slides, the author claims that the “Axiom of choice is trivial in intuitionistic logic” and that classical logic makes it a “ monster from outer space”. How is it trivial when it’s well known that the Axiom of Choice proves excluded middle?

I’ve seen another stack exchange post talking talking about the axiom in terms of relations, but the comment says that this is weaker than the actual axiom of choice which would explain why it doesn’t prove LEM.

Is this what the author was talking about, and if so, how does this weaker version relate to the full axiom?

  • 3
    $\begingroup$ what this comes down to is the difference between the $\Sigma$-types and its propositional truncated version $\exists$. I will write a long answer! $\endgroup$
    – Nico
    Apr 10 at 15:28
  • 3
    $\begingroup$ If you phrase AC in terms of "a family of inhabited sets has a choice function" (or some close approximation of this phrasing), then you're effectively requiring a uniform proof that all the sets in your family are inhabited which is tantamount to a proof that a choice function exists. $\endgroup$
    – Asaf Karagila
    Apr 10 at 15:42
  • 2
    $\begingroup$ One observation I can make: even if you consider that the axiom of choice is trivial for "constructible" proofs of every element of a family being nonempty, it becomes highly nontrivial again if you consider "the axiom of choice for setoids". For example, it's easy to provide a constructive proof that the projection $\mathbb{R} \to \mathbb{R} / \mathbb{Q}$ is surjective, even if your $\mathbb{R}$ is the constructive reals; but this proof does not result in a respectful right inverse of the projection. $\endgroup$ Apr 11 at 0:15
  • 1
    $\begingroup$ @DanielSchepler Iam not exactly sure what a hard axiom of choice is in that setting. when I have a term of $\Pi y:\mathbb R/\mathbb Q.\Sigma x:\mathbb R. y=[x]$, then I can extract an section of the quotient map, right? could you explain more? :) $\endgroup$
    – Nico
    Apr 11 at 6:21
  • 1
    $\begingroup$ What I mean is: if you treat $\mathbb{R} / \mathbb{Q}$ as the setoid whose elements are $\mathbb{R}$ and whose equality is set to congruence $\pmod{\mathbb{Q}}$, then $\lambda ([y] : \mathbb{R} / \mathbb{Q}) . (y, \mathrm{reflexivity})$ is respectful when you use the propositional truncation of $\sum x : \mathbb{R}, y = [x]$. But the extracted function $[y] \mapsto y$ is certainly not a respectful function $\mathbb{R} / \mathbb{Q} \to \mathbb{R}$; and if you could find a respectful section, that would give you a way to construct a non-measurable set, etc. etc. $\endgroup$ Apr 11 at 8:11

1 Answer 1


The right text to look at for more details is Andrej Bauer's text "Propositions as [Types]". You may also look at the paragraph "In Type Theory" of this nLab article, which explains the issue well. I can only speak about extensional type theory and its relation to categories and intuitionistic logic, since I do not have much experience with intensional type theory and HoTT.

The confusion comes from the fact that there are two ways to make "propositions as types" precise. Let me call the first one "proposition as proof-relevant types" and the second one "propositions as subsingelton types". In the nLab article they are called "propositions as all types" and "propositions as some types" respectively.

In the "proposition as proof-relevant types" world the existence quantifier corresponds to strong $\Sigma$-types. In that world something which looks like an axiom of choice is indeed valid. But there is no direct correspondence between the "propositions as proof-relevant types" logic and that what is normaly considered to be first-order many sorted intuitionistic logic. In particular, the proof of Diaconescu's theorem does not go through.

The kind of type theoretic logic that corresponds more directly to standard intuitionistic many-sorted first-order logic is the "propositions as subsingelton types" (or proof-irrelevant types) interpretation. This is also the version that people mean when they speak of the internal language/logic of a category. In that version the analogue of the axiom of choice is not automatically valid. More about that later.

Propositions as proof-relevant types

Extensional Martin-Löf dependent type theory comes per default with $\mathbf 1, \Sigma, \Pi$ and extensional equality. Let us look at an example to understand what "propositions as types" means. Consider the type $$\Pi m :\mathbb N.\Sigma n:\mathbb N.n>m$$ This type should intuitively be the type of proofs of the proposition "for all natural numbers $m$ there is a natural number $n$ such that $n$ is greater than $m$". Let me construct a term of that type. Say we already have a proof of the fact that for each $m:\mathbb N$ the natural number $S m$ is larger than $m$, where $S$ denotes the successor function. In the propositions as types language this means that we have a term $p: \Pi m:\mathbb N.Sm>m$. Then the following term will be "a proof" of the proposition we like to prove. $$ \lambda m.(Sm,p m): \Pi m:\mathbb N.\Sigma n:\mathbb N.n>m$$ Now when we have an actual natural number, for example $S0$, then we can apply our proof term to that number. $$(\lambda m.(Sm,p m))(S0) \equiv (SS 0, p(S0)) : \Sigma n:\mathbb N. n>S0$$ Here I use the $\equiv$-sign to denote judgemental equality. It is okay to understand this as "equal by definition" or "almost syntactically equal" from the categorical perspective, I hope no computer-scientist will kill me. We can now extract two components from the term of $\Sigma n:\mathbb N. n>S0$. The first component is a natural number $(SS0,p(S0)).1 \equiv SS0$, and the second component is a proof $(SS0,p(S0)).2 \equiv p(S0) : SS0 > S0$ of the fact that the natural number $SS0$ which we obtained from the first component is actually larger than the number $S0$ we started with. You can imagine that all types can be understood both as structures and as propositions. By inhabiting a type you do at the same time prove something. For example proving that prime numbers exist is arguably constructively the same activity as finding an inhabitent of the type of prime numbers.

The main point I am trying to make is that if $x:X\vdash Y\text{ type}$ is a dependent type (= a formula on $X$), then showing that "there is $x:X$ such that $Y(x)$ holds" is the same thing as inhabiting $\Sigma x:X.Y$. To do that we have to provide a term $t:X$ and a proof $p:Y[t/x]$. The pair $(t,p)$ will then be of type $\Sigma x:X.Y$. On the other hand, and this is crucially, we are able to extract from each proof $t:\Sigma x:X.Y$ both a term $t.1:X$ and a proof $t.2:Y[t.1/x]$ of the fact that $Y$ holds for $t.1$. This is exactly what won't be possible in the "proposition as subsingelton types" interpretation of logic.

Now what shall the axiom of choice be in this setting. Something which is reasonable (and works even without type theoretic universes) is the following "axiom scheme" (it is more a meta-property of the system than an actual axiom scheme).

(TTAC) Assume that $x:X\vdash Y \text{ type}$ is a family of types depending on another type $X$. If we can show that each $Y(x)$ is inhabited, then we may produce a choice function which chooses for each $x:X$ an element of $Y(x)$. This means we can produce a term of type $$(\Pi x:X.\Sigma y:Y(x).\mathbf 1)\to (\Pi x:X. Y(x))$$

The "type theoretic axiom of choice" in this version is just true. One can easily check that the judgement below is correct.

$$\lambda p. \lambda x. (p\, x).1 : (\Pi x:X.\Sigma y:Y(x).\mathbf 1)\to (\Pi x:X. Y(x))$$

I have put "axiom of choice" in quotation, since its categorical semantic isn't really what category theorists understand as the axiom of choice in a category. When our type theory has a universe $\mathcal U$, then another statement which looks reasonably like the axiom of choice is that the type $$\Pi X:\mathcal U. \Pi (Y:X\to \mathcal U). ((\Pi x:X.\Sigma y:Y\, x.\mathbf 1)\to (\Pi x:X. Y\,x))$$ is inhabited. But this is also just true, and it is not hard to produce a term of that type. This article here from the standford encylopedia of philosophy suggest that we should call the fact that we can always find an inhabitend of $$\Pi x:X.\Sigma y:Y. P(x,y)\to (\Sigma f:(X\to Y).\Pi x:X.P(x,f x))$$ the type theoretic axiom of choice. I am not exactly sure why, but as in the cases before, it is not hard to produce a term of that type!

Why does the type theoretic axiom of choice not imply the law of excluded middle? Well, we can look at a proof of Diaconescu's theorem and try to find out where we can no longer follow. When we go to section 3.7 of the article here (Intuitionism in the Philosophy of Mathematics - Standford Philosophy Encyclopedia) then we see that we have to form a "subset type" in the first step. What are subsets in type theory? Given some type $X$ and a predicate $x:X\vdash P(x) \text{ type}$ ranging over it, we like to form the type $\vdash \{x:X|P(x)\} \text{ type}$ of all $x:X$ which satisfy $P(x)$. So far we have no way of doing this. What maybe comes closest is the type $\Sigma x:X.P(x)$. After all, to produce a term of that type we need to provide at a term $t:X$ and a proof $p: P(t)$ that $t$ satisfies $P(t)$. But there is a problem: two different proofs $p,p':P(t)$ will give us distinct terms $(x,p)$ and $(x,p')$ of $\Sigma x:X.P(x)$, even though the element $x$ should really just appear once in the subset types. What we need is a mean is to somehow collapse the fibers of $P(x)$, so that for each $x:X$ the type $P(x)$ can have at most one term. Such a type is called a subsingelton type (or mono-type or mere proposition), and the process of collapsing the fibers of a type so that it becomes a mere proposition $[P(x)]$ is known under the name propositional truncation in type theory. The brackets [-] are a new type constructor whose rules in extensional type theory are described in Bauer's text which I mentioned at the beginning. The subset type is $\Sigma x:X.[P(x)]$. Let us now speak about the second type theoretic interpretation of logic.

Proposition as subsingelton types

This is a proof-irrelevant logic. Propositions are those types which contain at most one term. One says that a dependent type $\Gamma\vdash P \text{ type}$ is a subsingelton type when $$\Gamma, p:P,q:P\vdash p \equiv q:P$$ holds, i.e. when all terms of $P$ are judgementally equal. This makes sense because the judgementally equality sign $\equiv$ is part of the formal deductive system of Martin-Löf Type Theory. In the categorical semantic a type $\Gamma \vdash A\text{ type}$ is a subsingelton type if and only if the display map $p_A:\Gamma.A\to \Gamma$ of that type is a monomorphism. In the set-theoretic semantic of type theory $P$ is a subsingelton type if and only if each of its fibers contains at most one element. The type constructors $\Pi,\to$ and $=$ turn subsingelton types into subsingelton types, so we can still use them in the same way to interpret logic in type theory. The dependent sum type $\Sigma$ does not. Hence, to get a propositional truncated version $\exists$ of the existential quantifier, we need to always apply [-] after we apply $\Sigma$. For example the proof-irrelevant type-theoretical implementation of the proposition "for all $m:\mathbb N$ there is $n:\mathbb N$ such that $n>m$" is now $$\Pi m:\mathbb N.[\Sigma n:\mathbb N. n>m]$$ To produce (the necessarily unique) term of that type we still need to provide for each $m:\mathbb N$ a term $t(m):\mathbb N$ and a proof that $t(m)$ is greater than $m$. But we will no longer be able to extract from a proof of $\forall m:\mathbb N.\exists n:\mathbb N.n>m$ a function which provides such $n$s! The propositional truncation prevents this, the information is lost. How does "the axiom of choice" look like in this setting? A first version is the following axiom scheme.

(EAC) Whenever we have a dependent type $x:X \vdash Y(y)\text{ type}$ such that the subsingelton type $\forall x:X. \exists y:Y(x).\top$ is inhabited, then we may produce a term of type $\Pi x:X.Y(x)$.

The categorical semantic of that axiom scheme in a category is known under the name "external axiom of choice". "External" because the quantifiers which range over the sets $X$ and $Y$ come from the outside.

The categorical semantic of $\forall x:X.\exists y:Y(x).\top$ is that the image of the display map $p_Y: X.Y\to X$ is an epimorphism. A term of $\Pi x:X.Y(x)$ is the same thing as a section of the display map. Hence we see that (EAC) is valid in a category (with enough structure) when every regular epimorphism splits. When we have a meta-set-theory such as ZFC, then we will be able that EAC is valid in any category $Set_\kappa$ of sets up to a certain size, but when we work in a set theory without choice, such as ZF, then we will not be able that $Set_\kappa$ validates the external axiom of choice EAC for each cardinal. In particular this shows that the axiom of choice in the EAC version is not automatically valid in extensional type theory.

Remark. There is also an internal axiom of choice (IAC), where we also internalize the quantification over sets. To explain its meaning we would have to either introduce universes or the stack semantic of Mike Shulman, which is probably unnecessary to get the point across. The internal axiom of choice is weaker than EAC, but proving that the categories $Set_\kappa$ satisfy IAC does again require some amount of choice in the meta-set-theory.

Arguably, the axioms (EAC) and (IAC) correspond more closely to what we call "the axiom of choice" in set-theory. This is also witnessed by the fact that the categories $Set_\kappa$ always satisfy the type theoretic axiom of choice TTAC (as so does any other topos), but that the validity of EAC and IAC in $Set_\kappa$ depends on some amount of choice in the meta-theory. You can find a detailed comparison between the choice axioms in material set theory and choice in type theory in Mike Shulman's paper Stack Semantics and the Comparison of Material and Structural Set Theories. To read more about IAC and EAC you may look at the nLab article about choice.

Informal summary.

To prove constructively that each fiber of a family of sets is inhabited, you have to write down a method which produces inhabitants of the fibers for any given index. When you still remember your method of producing those inhabitants, then you are of course able to produce a choice function. This is the situation where "exists" is modeled through $\Sigma$-types. On the other hand, when you do not have access to the method and only know that a constructive proof exist (for example because another mathematician has announced that they have produced a constructive proof, but they are unwilling to publish it), then you can not write down a choice function constructively. This is the situation where your only information is that a proof exists, but all other information is lost (propositional truncation).

  • 8
    $\begingroup$ This is the most nontrivial explanation I've ever seen for why something is trivial $\endgroup$
    – Hong Ooi
    Apr 11 at 4:13

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .