Law of excluded middle from axiom of choice

(Part of the series Introduction to dependent type theory.)

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 $\mathsf{isProp}$ and $\mathsf{Prop}$ for the predicate and subuniverse of (-1)-types.

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

$$P+(P\to\mathbf{0})$$

where $P$ is an arbitrary (-1)-type.

Axioms #

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

$$\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 $I$ has to be a 0-type and $\phi(i,x)$ has to be a (-1)-type for all $i$ and $x$, $\phi:I\to A\to\mathsf{Prop}$, and $A$ is just any type, $A:\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:

$$\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 $A\simeq B$, which means that $A$ and $B$ are equivalent:

$$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, $f$ and $g$. It is easy to prove then – with the induction principle of equality – that

$$(f=g)\to\left(\prod_{x:A}\,f(x)=g(x)\right)$$

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

$$(f=g)\simeq\left(\prod_{x:A}\,f(x)=g(x)\right)$$

Similarly, for two propositions/(-1)-types, $P$ and $Q$, it is easy to prove that

$$(P=Q)\to\big((P\to Q)\times(Q\to P)\big)$$

but with propositional extensionality, it is again an equivalence:

$$(P=Q)\simeq\big((P\to Q)\times(Q\to P)\big)$$

Preliminaries #

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 $\mathbf{2}$ (the type with exactly two elements) has decidable equality; meaning that the following is inhabited:

$$\prod_{x,y:\mathbf{2}}(x=y)+\big((x=y)\to\mathbf{0}\big)$$

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

Proof:
We will explicitly construct a function of the above type. The defining characteristic of the type $\mathbf{2}$ is that in order to define a function on $\mathbf{2}$, it suffices to give a value for $f(0_2)$ and for $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 $\mathbf{2}$, we’ll have to specify four values. Here are the two easy ones:

Now, we still need $f(0_2, 1_2)$ and $f(1_2, 0_2)$, which are slightly trickier. Obviously, it will be $f(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:(0_2=1_2)$ then we can construct an element of $\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:A\to\mathcal{U}$ is a type-valued function, then we have

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

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

Therefore, equality on $\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:

$$\prod_{P,Q:\mathcal{U}}\mathsf{isProp}(P)\to\mathsf{isProp}(Q)\to\mathsf{isProp}(P=_\mathcal{U}Q)$$

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

Proof:
As a reminder, we have

$$\mathsf{isProp}(A):\equiv\prod_{x:A}\prod_{y:A}(x=y)$$

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

Now, let $\mu, \eta:(P=Q)$ and let $f$ be the equivalence between $(P=Q)$ and $((P\to Q)\times(Q\to P)\big)$ and let $g$ be its left-inverse (which exists because $f$ is an equivalence). Then, $f(\mu)=f(\eta)$ because the codomain of $f$ is a (-1)-type and $g(f(\mu))=g(f(\eta))$ because of induction on equality. Finally, we conclude $\mu=\eta$, because $g$ is the left-inverse. Thus, $(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:

$$\prod_{A:\mathcal{U}}\mathsf{isProp}(A)\to\mathsf{isSet}(A)$$

And as a reminder:

$$\mathsf{isSet}(A):\equiv\prod_{x,y:A}\mathsf{isProp}(x=_Ay)$$

Proving this is unfortunately a bit tedious.

Proof:
First recall the fact that equality is transitive:

$$\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)\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)$ and $q:(x=z)$, then then we can “concatenate” them to get a new witness: $\mathsf{trans}_{xyz}(p, q):(y=z)$.

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

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

That is, if I take a witness $p:(x=y)$ and concatenate it with itself, then what I get back should be equal to the reflexivity witness $\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:

$$\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 $R$, which may also depend on an equality witness $p:(x=y)$, then if that relation holds for $y\equiv x$ with the reflexivity witness $\mathsf{refl}_x$, then it holds for all $x$ and $y$ and for all witnesses.

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

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

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

$$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:\prod_{x,y:A}(x=_A\,y)\to C(x)\to C(y)$$

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

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

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

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

$$f:\prod_{x,y}(x=y)$$

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

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

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

$$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=y$ and $x=z$, and then concatenating them. The relation $R$ claims then that the resulting witness for $y=z$ is equal to $p$. In order to prove that this holds for all $p$, we again only have to prove the base case:

$$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: $\mathsf{trans}_{xyy}\big(p, p\big)=\mathsf{refl}_{y}$, so this is true. Then by induction, $R(y, z, p)$ holds for all $y$, $z$, and $p$.

Let’s define the shorthand

$$\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)$ implies that $p=h(y,z)$, and we know this is true for all $y$, $z$, and $p:(y=z)$. As equality is transitive, this also means $p=q$ for any $q:(y=z)$. And if we set $z\equiv x$, then we get what we wanted to prove:

$$\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

$$\prod_{A:\mathcal{U}}\mathsf{isProp}(\mathsf{isProp}(A))$$

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

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

Definition 1 #

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

$$\mathsf{Prop}:\equiv\sum_{A:\mathcal{U}}\mathsf{isProp}(A)$$

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

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

Main theorem #

We will now try to prove the following:

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

Setup #

In order to do this, we will first construct a type $I$ with two elements, $U,V:I$, that are equal if $P$ is inhabited: $U=V$ (in which case the type $I$ would behave as having only one element). This type $I$ 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 $P$ 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: $P$ is either inhabited or not, so $I$ 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 $P$ is inhabited or not, and so, we don’t know how many elements $I$ has. So, without LEM, it is impossible to prove that $I$ is finite.

So, let’s construct $U$ and $V$, which are equal if $P$ is inhabited. We construct them as propositions:

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

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

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

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

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

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

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

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

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

$$I:\equiv\sum_{Q:\mathsf{Prop}}\|(Q=U)+(Q=V)\|$$

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

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

Proof #

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

The first step is defining a function from $\mathbf{2}$ to $I$, 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:\mathbf{2}\to I$ be defined by $g(0_2)\equiv U$ and $g(1_2)\equiv V$. As already mentioned in the proof for Lemma 1, it suffices to specify the values for $0_2$ and $1_2$ when defining a function on $\mathbf{2}$.

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

$$\prod_{i:I}\left\|\sum_{x:\mathbf{2}}g(x)=i\right\|$$

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

$$\|(i=U)+(i=V)\|\to\left\|\sum_{x:\mathbf{2}}g(x)=i\right\|$$

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

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

$$\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 $f$ with the property that $g\circ f=id_I$, which implies that $f$ is injective.

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

$$\prod_{x,y:\mathbf{2}}(x=y)+\big((x=y)\to\mathbf{0}\big)$$

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

$$\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 $f$ on the left-hand side of this sum type and just general equality rules on the right-hand side to get:

$$\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 $g$:

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

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

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

and so we get

$$P+(P\to\mathbf{0})$$

This post is part of the series Introduction to dependent type theory.

• Previous post: Classical logic based on propositions-as-subsingleton-types