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 and for the predicate and subuniverse of (-1)-types.
What we want to prove is the law of excluded middle:
where is an arbitrary (-1)-type.
Our starting point is the axiom of choice (written as a type, as mentioned):
The index type has to be a 0-type and has to be a (-1)-type for all and , , and is just any type, . The double bars 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:
That is, an equivalence is a function with a left-inverse and a right-inverse. We can then define , which means that and are equivalent:
With this in mind, we can define the two additionally required axioms.
Consider two functions of the same function type, and . 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, and , it is easy to prove that
but with propositional extensionality, it is again an equivalence:
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 (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 is that in order to define a function on , it suffices to give a value for and for (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 , we’ll have to specify four values. Here are the two easy ones:
Now, we still need and , which are slightly trickier. Obviously, it will be , but how to construct the witness for that? We need to show that if we have a then we can construct an element of (aka, a contradiction).
Let’s recall the induction principle for equality. It states that “equals may be substituted for equals.” Formally: If is a type-valued function, then we have
So, if we define the type-valued function , with and , and we have , then the function , which is given by the induction principle above, can construct an element of with . Thus, we showed . And by symmetry, we also have .
Therefore, equality on 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 and be two (-1)-types. We need to show that is a (-1)-type. Because of propositional extensionality, this equality type is equivalent to . So, let’s investigate whether that type is a (-1)-type. Let and be elements of . Then and are equal by function extensionality, since for any because and are in , where all elements are equal to all other elements. A symmetrical argument holds for and , so , and thus, is a (-1)-type.
Now, let and let be the equivalence between and and let be its left-inverse (which exists because is an equivalence). Then, because the codomain of is a (-1)-type and because of induction on equality. Finally, we conclude , because is the left-inverse. Thus, 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:
This property follows immediately from the induction principle for equality stated above when we set .
Now, this theorem can also be interpreted as a function acting on equality witnesses. For example, if we have witnesses and , then then we can “concatenate” them to get a new witness: .
We can also prove that this function follows certain laws. For example, in the special case where , we can prove the following (which we’ll need to prove this lemma):
That is, if I take a witness and concatenate it with itself, then what I get back should be equal to the reflexivity witness .
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:
Let’s unpack this: if we have a relation , which may also depend on an equality witness , then if that relation holds for with the reflexivity witness , then it holds for all and and for all witnesses.
So, let’s express what we want to prove as a relation:
where may be any element of . To prove that this holds for all , and , it suffices to prove the base case where and :
And this follows from the fact that in the (simplified) induction principle:
the mapping is guaranteed to be the identity function if the given equality witness for is the reflexivity witness. This implies
for all (with judgmental equality even). With this, we can immediately prove , which then implies for any , and .
OK, this was just our setup. Now, let’s try to prove that for any , all the equality witnesses are the same. We know that is a (-1)-type, which means there is a function with the following type:
For any two elements of , this function gives us an equality witness.
The idea of the proof is now that we can represent any witness as a concatenation of outputs of . Which will then imply that all witnesses are equal to each other.
First, we fix and then define the following relation:
So, what we are doing here is looking up the witnesses for and , and then concatenating them. The relation claims then that the resulting witness for is equal to . In order to prove that this holds for all , we again only have to prove the base case:
But this is exactly what we proved above: , so this is true. Then by induction, holds for all , , and .
Let’s define the shorthand
Thus, implies that , and we know this is true for all , , and . As equality is transitive, this also means for any . And if we set , then we get what we wanted to prove:
Hence, every (-1)-type is also a 0-type.
Corollary 1 #
An easy corollary of the previous proof is
That is: the judgment is itself a (-1)-type.
So, let . Given that we have witnesses for , we know that is a (-1)-type and by the previous lemma, also a 0-type. The codomain of and is where . As is a 0-type, everything in the codomain is equal to each other. So, by function extensionality, and are equal and hence, is a (-1)-type for any type .
Definition 1 #
Now, given that is a (-1)-type, we can define the subuniverse of (-1)-types:
This kind of definition only works if the predicate after the -sign always returns (-1)-types, because otherwise there could be multiple witnesses and , and then elements could appear twice in : and .
But if is a proper (-1)-type, then elements from can appear at most once in , as it should be.
Main theorem #
We will now try to prove the following:
In order to do this, we will first construct a type with two elements, , that are equal if is inhabited: (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 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: is either inhabited or not, so 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 is inhabited or not, and so, we don’t know how many elements has. So, without LEM, it is impossible to prove that is finite.
So, let’s construct and , which are equal if is inhabited. We construct them as propositions:
If is inhabited, then both and are inhabited, and so by propositional extensionality, we have in that case. This shows that .
In order for the proof to succeed, we also need to show the inverse:
because the axiom of choice will allows us to conclude that is either equal to or not: , and then we will only need to replace with to complete the proof.
So, let’s assume and expand the definition:
As discussed above, this implies (among other things) . But is always inhabited by (the truncated version of ). Hence, must also be inhabited. So, it just remains to be shown that . Since is a (-1)-type, we may assume the untruncated in order to prove . So, we can do a case analysis on : if , then obviously we have and are done; if , then by the fact that we have for any type , we may also conclude (though of course, as long as the theory is consistent, it will be impossible to construct an element of ). Thus, we have proved from .
Finally, we need a type that contains only and . We simply define it has a subuniverse of :
We have proved in Lemma 2 that equality among propositions is a proposition as well, so is a 0-type, as required in the conditions for the axiom of choice.
The setup is now complete: we have a 0-type such that if equality is decidable on , the law of excluded middle holds for .
In the main proof we will show that with the axiom of choice, the fact that equality is decidable on (see Lemma 1) implies that it’s also decidable on .
The first step is defining a function from to , 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 be defined by and . As already mentioned in the proof for Lemma 1, it suffices to specify the values for and when defining a function on .
Now, to show that is surjective, we have to prove the following:
So, let . From the definition of , we know that . Meaning we have to prove the following:
By the rules of propositional truncation, we may assume that we have either or . However, from the definition of , we can see that both cases are well covered: and . Therefore, is surjective.
We are now ready to apply AC in order to get the right-inverse of . Setting and replacing with in the axiom as stated in the beginning, we get this:
As you can see, the conditions for the axiom are fulfilled and so the axiom of choice hands us a function with the property that , which implies that is injective.
Now, let’s combine those facts with the result of Lemma 1 – the fact that has decidable equality:
We will choose and :
We use the injectiveness of on the left-hand side of this sum type and just general equality rules on the right-hand side to get:
Then, we’ll just use the definition of :
This means that equality is decidable on ! We already showed above that
and so we get
This post is part of the series Introduction to dependent type theory.
- Previous post: Classical logic based on propositions-as-subsingleton-types