§ Diaconescu's theorem

• Choice implies LEM
• Let $P$ be a proposition. Build the sets $T, F$ as:
• $T \equiv {x \in \{0, 1\} : (x = 1) \lor P}$, and $F \equiv x \in \{ 0, 1 \} : (x = 0) \lor P \}$.
• Note that if we had LEM, we could case split on $P$ via LEM and show that $x \equiv \{ 1 \}$ if $P$, and $x \equiv \{ 0, 1\}$ if $\not P$.
• However, we don't have LEM. So let's invoke Choice on the set $B \equiv \{T, F \}$. This means we get a choice function $c: B \to \cup c B$ such that $c(T) \in T$ and $c(F) \in F$.
• By the definition of the two sets, this means that $(c(T) = 1 \lor P)$, and $(c(F) = 0 \lor P)$.
• This can be written as the logical formula $(c(T) = 1 \lor P) \land (c(F) = 0 \lor P)$.
• This is the same as $(c(T) \neq c(F)) \lor P$.
• Now see that since $P \implies (U = V)$ (by extensionality), we have that $P \implies (f(U) = f(V))$.
• See that contraposition is available purely intuitionistically: ( (p -> q) -> (q -> false) -> p -> false).
• Therefore, by contraposition $(f(U) \neq f(V)) \implies \lnot P$.
• This means we have $P \lor \lnot P$!