## § 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$!