François G. Dorais

Research in Logic and Foundations of Mathematics


Diaconescu's Theorem

Diaconescu (1975) showed that the Axiom of Choice implies the Principle of Excluded Middle. More specifically, he showed that every topos that satisfies (a very mild form of) the Axiom of Choice is Boolean. Diaconescu’s argument applies in many other contexts too. In this post, I will present a variant of that argument. I will keep the context of the argument deliberately ambiguous to demonstrate its broad applicability.

A set is decidable if holds for all In other words, is decidable if the diagonal is complemented in The empty set and singleton sets are trivially decidable, but some more complicated sets are decidable too. For example, one can use induction to show that the set of natural numbers is decidable. This and the following fact shows that every set of natural numbers, in particular is also decidable.

If is an injection and is decidable then is also decidable.

This is because an is an injection precisely when for all Since by hypothesis, we conclude that too. A set is choice if every surjection splits (there is a map such that ). Thus, the Axiom of Choice says that every set is choice. Decidability and choiceness play together very well.

If is a surjection and is a decidable choice set, then is also a decidable choice set.

Indeed, the surjection has a splitting which is necessarily an injection; it follows that is decidable. To see that is choice, suppose that is a surjection. Then is a surjection too and therefore there is a splitting such that But then is a splitting of

If is a choice set then equality is decidable.

To see this, note that for all we have a surjection Since is decidable, it follows that if is a choice set then is decidable (and choice), hence

Now given a formula we may use comprehension to form the set (where does not occur free in ). Since we see that This completes the proof that:

If is a choice set then the Principle of Excluded Middle holds.

As you can see, the above argument goes through with very few assumptions. Pairing alone can be used to construct and even the graph of the surjection We implicitly used the set of natural numbers but we didn’t really need the entire set of natural numbers. We only used the fact that and any two distinct objects and would work just as well. So pairing and nontriviality are sufficient to show that equality is decidable. Finally, we used a rather tame form of comprehension to get the decidability of any formula. Although some set theories do restrict comprehension, they all allow a certain amount of comprehension and this argument still has nontrivial conclusions in such contexts.

A side effect of this result is the implausibility of set-theoretic semantics for constructive mathematics. Indeed, constructivism rejects the Principle of Excluded Middle but accepts the Axiom of Choice since choice is implicit in the constructive meaning of existence. So constructivism is incompatible with Diaconescu’s result. How is this possible? The argument I presented looks perfectly constructive except perhaps for the ultimate use of comprehension, which could be impredicative. Even then, decidability of equality is enough to demonstrate incompatibility since constructivists reject the decidability of equality for real numbers.

It so happens that one very important aspect of the argument is non constructive. It is so well hidden that you probably haven’t noticed how often the Axiom of Extensionality was used in the above argument! Extensionality is not compatible with constructivism since constructions are inherently intensional. In a constructive set, each element comes with extra baggage. It is that extra baggage that allows us to choose elements from inhabited sets. So if we accept the above justification for the Axiom of Choice then we must reject the Axiom of Extensionality. In this context, Diaconescu’s result only tells us that intensional equality is decidable: we can always tell whether the processes that generate and are the same or different. Whether the outcome of two processes is the same or not is an entirely different matter. To make the doubleton extensional, we should include all possible ways of constructing and With all this extra baggage, we may not have a surjection and the argument falls apart.

Of course, there are constructive theories that are extensional, such as Aczel’s CZF, but these theories reject the Axiom of Choice. On the other hand, Martin-Löf’s constructive type theory (ML) is an example of an intensional constructive theory. Ironically, Aczel’s interpretation of CZF in ML makes extensive use of the fact that ML validates the Axiom of Choice.

References

  1. R. Diaconescu, 1975: Axiom of choice and complementation, Proc. Amer. Math. Soc. 51, 176–178.


CC0 Originally posted on by François G. Dorais. To the extent possible under law, François G. Dorais has waived all copyright and neigboring rights to this work.


Comments