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 settheoretic 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, MartinLö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

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

mr: 0373893

zbl: 0317.02077

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

François G. Dorais wrote
Andrej Bauer presents a slick proof of Diaconescu’s theorem in this IAS video. Here is his argument…
Let and let be a proposition (which doesn’t depend on ). Consider the sets
These are inhabited sets so there is a choice function Since is decidable, we have In the first case, must hold for if then and hence and if then and hence If then we must have and thus Therefore, we conclude that

Rafal wrote
Is there an easy example of a set which is not decidable in the abovementioned sense?

François G. Dorais replied to Rafal
In order to have a counterexample, you need to be in a nonclassical setting. The counterexample will depend on that setting. In classical settings, every set is decidable. In constructive settings, is an example of a set which is not decidable (see Brouwer’s counterexamples).
The argument above gives a counterexample assuming the existence of some statement such that is not true. In that case, the set is not decidable since is equivalent to . Of course, and this is the main point of my post, this example uses extensionality.

Rafal replied to François G. Dorais
Thanks for the link. Just one question: what is , the exponent of in the second clause of the definition of the Cauchy sequence (in the linked SEP entry)? I suppose it is to be the smallest among those numbers which falsify the Goldbach’s conjecture and thus the sequence stabilizes on some fixed rational number . Otherwise it makes little sense to me, as is bounded by the existential quantifier.

François G. Dorais replied to Rafal
You are correct. That Brouwer counterexample is the alternating sequence unless a counterexample to Goldbach (or an occurrence of consecutive ’s in the digits of , etc.) has been found before , in which case where is that first counterexample.