Thomas M. Kehrenberg

Law of excluded middle from axiom of choice

(Part of the series .)

This is a proof of the law of excluded middle from the (type-theoretic) axiom of choice, propositional extensionality and function extensionality.

We take as background dependent type theory with dependent product types and identity types.

As we have to be very careful to only use intuitionistic logic for this proof, I will not use any logic notation. Instead, everything is written in pure types. I will also try to use the most standard notation, which means, for example, using isProp\mathsf{isProp} and Prop\mathsf{Prop} for the predicate and subuniverse of (-1)-types.

What we want to prove is the law of excluded middle:


where PP is an arbitrary (-1)-type.


Our starting point is the axiom of choice (written as a type, as mentioned):

(i:Ix:Aϕ(i,x))f:IAi:Iϕ(i,f(i))\left(\prod_{i:I}\left\|\sum_{x:A}\phi(i, x)\right\| \right)\to \left\| \sum_{f:I\to A}\prod_{i:I}\phi\big(i, f(i)\big) \right\|

The index type II has to be a 0-type and ϕ(i,x)\phi(i,x) has to be a (-1)-type for all ii and xx, ϕ:IAProp\phi:I\to A\to\mathsf{Prop}, and AA is just any type, A:UA:\mathcal{U}. The double bars \|\dots\| represent propositional truncation, which we assume as an additional part of our theory. Note that without function extensionality, the axiom above is not necessarily a (-1)-type, but it’s not strictly required that it is a (-1)-type, so we don’t need function extensionality quite yet (though we will definitely need it later).

In addition to the axiom of choice, we will need two other axioms. They will be formulated as equivalences, so we quickly recall the definition of an equivalence:

isequiv(f):g:BAa:A(g(f(a))=Aa)×h:BAb:B(f(h(b))=Bb)\mathsf{isequiv}(f):\equiv\sum_{g:B\to A}\prod_{a:A}\Big(g(f(a))=_Aa\Big) \times\sum_{h:B\to A}\prod_{b:B}\Big(f(h(b))=_Bb\Big)

That is, an equivalence is a function with a left-inverse and a right-inverse. We can then define ABA\simeq B, which means that AA and BB are equivalent:

AB:f:ABisequiv(f)A\simeq B:\equiv\sum_{f:A\to B}\mathsf{isequiv}(f)

With this in mind, we can define the two additionally required axioms.

Consider two functions of the same function type, ff and gg. It is easy to prove then – with the induction principle of equality – that


but the axiom of function extensionality now asserts that the above is an equivalence:


Similarly, for two propositions/(-1)-types, PP and QQ, it is easy to prove that

(P=Q)((PQ)×(QP))(P=Q)\to\big((P\to Q)\times(Q\to P)\big)

but with propositional extensionality, it is again an equivalence:

(P=Q)((PQ)×(QP))(P=Q)\simeq\big((P\to Q)\times(Q\to P)\big)


Before we get to the main theorem, we’ll get a few smaller proofs out of the way, so that they won’t distract us later.

Lemma 1

Let’s start with something easy: prove that 2\mathbf{2} (the type with exactly two elements) has decidable equality; meaning that the following is inhabited:


So, any two elements are either equal or explicitly not equal.

We will explicitly construct a function of the above type. The defining characteristic of the type 2\mathbf{2} is that in order to define a function on 2\mathbf{2}, it suffices to give a value for f(02)f(0_2) and for f(12)f(1_2) (this is just a fancy way of saying “the type has exactly two elements”).

So, given that the above function type has two arguments of type 2\mathbf{2}, we’ll have to specify four values. Here are the two easy ones:

xx yy f(x,y)f(x,y) inhabitant of f(x,y)f(x,y)
020_2 020_2 02=020_2=0_2 refl0\mathsf{refl}_0
121_2 121_2 12=121_2=1_2 refl1\mathsf{refl}_1

Now, we still need f(02,12)f(0_2, 1_2) and f(12,02)f(1_2, 0_2), which are slightly trickier. Obviously, it will be f(02,12)(02=12)0f(0_2, 1_2)\equiv(0_2=1_2)\to\mathbf{0}, but how to construct the witness for that? We need to show that if we have a p:(02=12)p:(0_2=1_2) then we can construct an element of 0\mathbf{0} (aka, a contradiction).

Let’s recall the induction principle for equality. It states that “equals may be substituted for equals.” Formally: If C:AUC:A\to\mathcal{U} is a type-valued function, then we have

g:x,y:A(x=Ay)C(x)C(y)g:\prod_{x,y:A}(x=_A\,y)\to C(x)\to C(y)

So, if we define the type-valued function CC, with C(02)1C(0_2)\equiv\mathbf{1} and C(12)0C(1_2)\equiv\mathbf{0}, and we have p:(02=12)p:(0_2=1_2), then the function gg, which is given by the induction principle above, can construct an element of 0\mathbf{0} with g(02,12,p,)g(0_2, 1_2, p, \star). Thus, we showed (02=12)0(0_2=1_2)\to\mathbf{0}. And by symmetry, we also have (12=02)0(1_2=0_2)\to\mathbf{0}.

Therefore, equality on 2\mathbf{2} is decidable.

Lemma 2

The next thing we need to prove is that the equality type for (-1)-types is a (-1)-type as well:


We’ll require both propositional and function extensionality for this.

As a reminder, we have


So, let PP and QQ be two (-1)-types. We need to show that P=QP=Q is a (-1)-type. Because of propositional extensionality, this equality type is equivalent to ((PQ)×(QP))((P\to Q)\times(Q\to P)\big). So, let’s investigate whether that type is a (-1)-type. Let (u,v)(u,v) and (u,v)(u', v') be elements of ((PQ)×(QP))((P\to Q)\times(Q\to P)\big). Then uu and uu' are equal by function extensionality, since u(p)=u(p)u(p)=u'(p) for any p:Pp:P because u(p)u(p) and u(p)u'(p) are in QQ, where all elements are equal to all other elements. A symmetrical argument holds for vv and vv', so (u,v)=(u,v)(u,v)=(u', v'), and thus, ((PQ)×(QP))((P\to Q)\times(Q\to P)\big) is a (-1)-type.

Now, let μ,η:(P=Q)\mu, \eta:(P=Q) and let ff be the equivalence between (P=Q)(P=Q) and ((PQ)×(QP))((P\to Q)\times(Q\to P)\big) and let gg be its left-inverse (which exists because ff is an equivalence). Then, f(μ)=f(η)f(\mu)=f(\eta) because the codomain of ff is a (-1)-type and g(f(μ))=g(f(η))g(f(\mu))=g(f(\eta)) because of induction on equality. Finally, we conclude μ=η\mu=\eta, because gg is the left-inverse. Thus, (P=Q)(P=Q) is a (-1)-type.

Lemma 3

The final thing we need to prove in the preliminaries is that any (-1)-type is also a 0-type:


And as a reminder:


Proving this is unfortunately a bit tedious.

First recall the fact that equality is transitive:

trans:x,y,z:A(x=y)(x=z)(y=z)\mathsf{trans}:\prod_{x,y,z:A} (x=y)\to(x=z)\to(y=z)

This property follows immediately from the induction principle for equality stated above when we set C(x)(x=z)C(x)\equiv (x=z).

Now, this theorem can also be interpreted as a function acting on equality witnesses. For example, if we have witnesses p:(x=y)p:(x=y) and q:(x=z)q:(x=z), then then we can “concatenate” them to get a new witness: transxyz(p,q):(y=z)\mathsf{trans}_{xyz}(p, q):(y=z).

We can also prove that this function follows certain laws. For example, in the special case where zyz\equiv y, we can prove the following (which we’ll need to prove this lemma):

p:(x=y)transxyy(p,p)=refly\prod_{p:(x=y)}\mathsf{trans}_{xyy}\big(p, p\big)=\mathsf{refl}_{y}

That is, if I take a witness p:(x=y)p:(x=y) and concatenate it with itself, then what I get back should be equal to the reflexivity witness refly\mathsf{refl}_y.

In order to prove this, the induction principle from above is not sufficient, because it doesn’t make any mention of the witnesses. We will instead need the full “path induction” principle:

R:Πx,y:A(x=y)U(x:AR(x,x,reflx))x,y:Ap:(x=y)R(x,y,p)\prod_{R:\Pi_{x,y:A}(x=y)\to\mathcal{U}} \left( \prod_{x:A}R\big(x,x,\mathsf{refl}_x\big) \right) \to \prod_{x,y:A}\prod_{p:(x=y)}R(x,y,p)

Let’s unpack this: if we have a relation RR, which may also depend on an equality witness p:(x=y)p:(x=y), then if that relation holds for yxy\equiv x with the reflexivity witness reflx\mathsf{refl}_x, then it holds for all xx and yy and for all witnesses.

So, let’s express what we want to prove as a relation:

R(x,y,p)[transxyy(p,p)=refly]R(x, y,p)\equiv\Big[\mathsf{trans}_{xyy}\big(p, p\big)=\mathsf{refl}_{y}\Big]

where pp may be any element of (x=y)(x=y). To prove that this holds for all xx, yy and pp, it suffices to prove the base case where yxy\equiv x and preflxp\equiv \mathsf{refl}_x:

R(x,x,reflx)[transxxx(reflx,reflx)=reflx]R(x, x,\mathsf{refl}_x)\equiv \Big[\mathsf{trans}_{xxx}\big(\mathsf{refl}_x, \mathsf{refl}_x\big)=\mathsf{refl}_{x}\Big]

And this follows from the fact that in the (simplified) induction principle:

g:x,y:A(x=Ay)C(x)C(y)g:\prod_{x,y:A}(x=_A\,y)\to C(x)\to C(y)

the mapping C(x)C(y)C(x)\to C(y) is guaranteed to be the identity function idC(x)\mathsf{id}_{C(x)} if the given equality witness for (x=Ay)(x=_Ay) is the reflexivity witness. This implies

transxxz(reflx,p)p\mathsf{trans}_{xxz}\big(\mathsf{refl}_x, p\big)\equiv p

for all p:(x=z)p:(x=z) (with judgmental equality even). With this, we can immediately prove R(x,x,reflx)R(x, x,\mathsf{refl}_x), which then implies transxyy(p,p)=refly\mathsf{trans}_{xyy}\big(p, p\big)=\mathsf{refl}_{y} for any xx, yy and pp.

OK, this was just our setup. Now, let’s try to prove that for any x,y:Ax,y:A, all the equality witnesses are the same. We know that AA is a (-1)-type, which means there is a function with the following type:


For any two elements of AA, this function gives us an equality witness.

The idea of the proof is now that we can represent any witness p:(x=y)p:(x=y) as a concatenation of outputs of ff. Which will then imply that all witnesses are equal to each other.

First, we fix x:Ax:A and then define the following relation:

R(y,z,p)[transxyz(f(x,y),f(x,z))=p]R(y,z,p)\equiv\Big[\mathsf{trans}_{xyz}\big(f(x,y), f(x,z)\big)=p\Big]

So, what we are doing here is looking up the witnesses for x=yx=y and x=zx=z, and then concatenating them. The relation RR claims then that the resulting witness for y=zy=z is equal to pp. In order to prove that this holds for all pp, we again only have to prove the base case:

R(y,y,refly)[transxyy(f(x,y),f(x,y))=refly]R(y,y,\mathsf{refl}_y)\equiv\Big[\mathsf{trans}_{xyy}\big(f(x,y), f(x,y)\big)=\mathsf{refl}_y\Big]

But this is exactly what we proved above: transxyy(p,p)=refly\mathsf{trans}_{xyy}\big(p, p\big)=\mathsf{refl}_{y}, so this is true. Then by induction, R(y,z,p)R(y, z, p) holds for all yy, zz, and pp.

Let’s define the shorthand

h:y,z:A(y=z)h(y,z):transxyz(f(x,y),f(x,z))\begin{aligned} &h:\prod_{y,z:A}(y=z)\\ &h(y,z):\equiv\mathsf{trans}_{xyz}\big(f(x,y), f(x,z)\big) \end{aligned}

Thus, R(y,z,p)R(y,z,p) implies that p=h(y,z)p=h(y,z), and we know this is true for all yy, zz, and p:(y=z)p:(y=z). As equality is transitive, this also means p=qp=q for any q:(y=z)q:(y=z). And if we set zxz\equiv x, then we get what we wanted to prove:

x,y:Ap,q:(x=Ay)p=q\prod_{x,y:A}\prod_{p,q:(x=_Ay)} p=q

Hence, every (-1)-type is also a 0-type.

Corollary 1

An easy corollary of the previous proof is


That is: the judgment isProp(A)\mathsf{isProp}(A) is itself a (-1)-type.

So, let f,g:isProp(A)f,g:\mathsf{isProp}(A). Given that we have witnesses for isProp(A)\mathsf{isProp}(A), we know that AA is a (-1)-type and by the previous lemma, also a 0-type. The codomain of ff and gg is x=Ayx=_Ay where x,y:Ax,y:A. As AA is a 0-type, everything in the codomain is equal to each other. So, by function extensionality, ff and gg are equal and hence, isProp(A)\mathsf{isProp}(A) is a (-1)-type for any type AA.

Definition 1

Now, given that isProp(A)\mathsf{isProp}(A) is a (-1)-type, we can define the subuniverse of (-1)-types:


This kind of definition only works if the predicate after the \sum-sign always returns (-1)-types, because otherwise there could be multiple witnesses pp and qq, and then elements could appear twice in Prop\mathsf{Prop}: (P,p)(P, p) and (P,q)(P, q).

But if isProp(A)\mathsf{isProp}(A) is a proper (-1)-type, then elements from U\mathcal{U} can appear at most once in Prop\mathsf{Prop}, as it should be.

Main theorem

We will now try to prove the following:

P:UisProp(P)(P+(P0))\prod_{P:\mathcal{U}}\mathsf{isProp}(P)\to \Big(P+(P\to\mathbf{0})\Big)


In order to do this, we will first construct a type II with two elements, U,V:IU,V:I, that are equal if PP is inhabited: U=VU=V (in which case the type actually only has one element). This type will then be our index type when using the axiom of choice.

My first thought when reading about this proof was: “Doesn’t that mean the index set is finite? Which means we don’t even need AC?” (Since the finite version of the axiom of choice is a theorem in type theory.)

But why did I think that the type I described above was finite? My reasoning had been something like this: “regardless of whether PP is inhabited or not, the index type can have at most 2 elements, so it’s definitely finite.” But this reasoning implicitly used the law of excluded middle! Sure, in classical logic I can reason: PP is either inhabited or not, so II either has one or has two elements. But intuitionistic logic also allows a weird third case where we just can’t say anything about whether PP is inhabited or not, and so, we don’t know how many elements II has. So, without LEM, it is impossible to prove that II is finite.

So, let’s construct UU and VV, which are equal if PP is inhabited. We construct them as propositions:

U:0+PV:1+P\begin{aligned} U&:\equiv \|\mathbf{0}+P\|\\ V&:\equiv \|\mathbf{1}+P\| \end{aligned}

If PP is inhabited, then both UU and VV are inhabited, and so by propositional extensionality, we have U=VU=V in that case. This shows that P(U=V)P\to(U=V).

In order for the proof to succeed, we also need to show the inverse:

(U=V)P(U=V)\to P

because the axiom of choice will allows us to conclude that UU is either equal to VV or not: (U=V)+((U=V)0)(U = V)+\big((U = V)\to\mathbf{0}\big), and then we will only need to replace U=VU=V with PP to complete the proof.

So, let’s assume U=VU=V and expand the definition:

0+P=1+P\|\mathbf{0}+P\|= \|\mathbf{1}+P\|

As discussed above, this implies (among other things) 1+P0+P\|\mathbf{1}+P\|\to \|\mathbf{0}+P\|. But 1+P\|\mathbf{1}+P\| is always inhabited by |\star| (the truncated version of :1\star:\mathbf{1}). Hence, 0+P\|\mathbf{0}+P\| must also be inhabited. So, it just remains to be shown that 0+PP\|\mathbf{0}+P\|\to P. Since PP is a (-1)-type, we may assume the untruncated 0+P\mathbf{0}+P in order to prove PP. So, we can do a case analysis on 0+P\mathbf{0}+P: if PP, then obviously we have PP and are done; if 0\mathbf{0}, then by the fact that we have 0A\mathbf{0}\to A for any type AA, we may also conclude PP (though of course, as long as the theory is consistent, it will be impossible to construct an element of 0\mathbf{0}). Thus, we have proved PP from U=VU=V.

Finally, we need a type that contains only UU and VV. We simply define it has a subuniverse of Prop\mathsf{Prop}:


We have proved in Lemma 2 that equality among propositions is a proposition as well, so II is a 0-type, as required in the conditions for the axiom of choice.

The setup is now complete: we have a 0-type II such that if equality is decidable on II, the law of excluded middle holds for PP.


In the main proof we will show that with the axiom of choice, the fact that equality is decidable on 2\mathbf{2} (see Lemma 1) implies that it’s also decidable on II.

The first step is defining a function from 2\mathbf{2} to II, which we will prove to be surjective. We’ll then use the axiom of choice to pick a right-inverse for this function.

So, let the function g:2Ig:\mathbf{2}\to I be defined by g(02)Ug(0_2)\equiv U and g(12)Vg(1_2)\equiv V. As already mentioned in the proof for Lemma 1, it suffices to specify the values for 020_2 and 121_2 when defining a function on 2\mathbf{2}.

Now, to show that gg is surjective, we have to prove the following:


So, let i:Ii:I. From the definition of II, we know that (i=U)+(i=V)\|(i=U)+(i=V)\|. Meaning we have to prove the following:


By the rules of propositional truncation, we may assume that we have either i=Ui=U or i=Vi=V. However, from the definition of gg, we can see that both cases are well covered: g(02)Ug(0_2)\equiv U and g(12)Vg(1_2)\equiv V. Therefore, gg is surjective.

We are now ready to apply AC in order to get the right-inverse of gg. Setting ϕ(i,x):(g(x)=i)\phi(i, x):\equiv(g(x)=i) and replacing AA with 2\mathbf{2} in the axiom as stated in the beginning, we get this:

(i:Ix:2g(x)=i)f:I2i:Ig(f(i))=i\left(\prod_{i:I}\left\|\sum_{x:\mathbf{2}}g(x)=i\right\| \right)\to \left\| \sum_{f:I\to \mathbf{2}}\prod_{i:I}g\big(f(i)\big)=i \right\|

As you can see, the conditions for the axiom are fulfilled and so the axiom of choice hands us a function ff with the property that gf=idIg\circ f=id_I, which implies that ff is injective.

Now, let’s combine those facts with the result of Lemma 1 – the fact that 2\mathbf{2} has decidable equality:


We will choose x:f(g(02))x:\equiv f(g(0_2)) and y:f(g(12))y:\equiv f(g(1_2)):

(f(g(02))=f(g(12)))+((f(g(02))=f(g(12)))0)\Big(f\big(g(0_2)\big) = f\big(g(1_2)\big)\Big)+\bigg(\Big(f\big(g(0_2)\big) = f\big(g(1_2)\big)\Big)\to\mathbf{0}\bigg)

We use the injectiveness of ff on the left-hand side of this sum type and just general equality rules on the right-hand side to get:

(g(02)=g(12))+((g(02)=g(12))0)\big(g(0_2) = g(1_2)\big)+\Big(\big(g(0_2) = g(1_2)\big)\to\mathbf{0}\Big)

Then, we’ll just use the definition of gg:

(U=V)+((U=V)0)\big(U = V\big)+\Big(\big(U = V\big)\to\mathbf{0}\Big)

This means that equality is decidable on II! We already showed above that

(P(U=V))×((U=V)P)\big(P\to (U=V)\big)\times \big((U=V)\to P\big)

and so we get




This post is part of the series .