§ Diaconescu's theorem
- Choice implies LEM
- Let be a proposition. Build the sets as:
- , and .
- Note that if we had LEM, we could case split on via LEM and show that if , and if .
- However, we don't have LEM. So let's invoke Choice on the set . This means we get a choice function such that and .
- By the definition of the two sets, this means that , and .
- This can be written as the logical formula .
- This is the same as .
- Now see that since (by extensionality), we have that .
- See that contraposition is available purely intuitionistically: (
(p -> q) -> (q -> false) -> p -> false).
- Therefore, by contraposition .
- This means we have !