Diaconescu's Theorem

by William DeMeo - - posted in Notes

I learned about Diaconescu’s Theorem from Andrej Bauer’s lecture.

This post describes the proof as it was presented by Bauer. These notes are rough and intended for my own reference. Please see François Dorais’ blog post for a nice discussion of this topic.

  • The Axiom of Choice (AC) states that if $\mathcal{S}$ is a collection of nonempty sets, then there is a choice function $f$ that can be used to select an element from each set in $\mathcal{S}$.

  • Law of the Excluded Middle (LEM) states that $P$ is a proposition, then $P \bigvee \neg P$.

  • Diaconescu’s Theorem: AC $\rightarrow$ LEM.

    Proof: Assume AC. Let $P$ be any proposition. We will prove $P \bigvee \neg P$.

    Define the set $\mathbf{2} = \{0, 1\} = \{x \mid x = 0 \bigvee x= 1\}$.

    Define the following sets:

    Note that $P \Rightarrow A = B = \mathbf{2}$. Therefore, $A \neq B \Rightarrow \neg P$.

    Both of the sets $A$ and $B$ are nonempty, since 0 belongs to $A$ and 1 belongs to $B$.

    Therefore, $\{A, B\}$ is a set of nonempty sets, so by AC we have a choice function,

    Now, because equality on $\mathbb{N}$ is decidabile (which can be proved by induction on $\mathbb{N}$), we can consider cases:

    If $f(A) = 0 = f(B)$, then $0 \in B$, so $P$.

    If $f(A) = 1 = f(B)$, then $1 \in A$, so $P$.

    If $f(A) \neq f(B)$, then $A \neq B$ so $P$ cannot hold. (Recall, $P \Rightarrow A = B = \mathbf{2}$.)

    We have covered all cases and found that $P \bigvee \neg P$ holds. ∎

Coq

Proofs of Diaconescu’s Theorem in Coq

Appendix

  • Decidable Sets. A set $S$ is decidable if for all $x, y \in S$ we have $x = y \bigvee x \neq y$. 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.

References