Intuition for Diaconescu's theorem

Question

Diaconescu's theorem proves that the axiom of choice implies the law of the excluded middle.

While I can follow the proof in the above wikipedia article, it just seems like a cheap trick, so to speak, rather than something deep going on.

Specifically, I'm trying to think of an intuitive way of understanding the contrapositive (haha -- but this is okay, because we can prove $(p\to q)\to(\neg q \to \neg p)$ without the law of the excluded middle, just not the converse) of the statement in the context of type theory.

Here, the law of the excluded middle essentially states "all propositions are either empty or the universe" -- so the contrapositive of Diaconescu's theorem says "if there is a proposition that is neither empty nor the universe, you can't always have a choice function".

This seems to me to be a promising route to understanding the theorem, but I can't finish my train of thought -- do "middle" propositions not permit a choice function? Does that make sense? Is there another way to understand the proof more intuitively?

Answer 1

Based on your terminology and comments, you seem to be having an internal versus external/syntax versus semantics confusion.

Syntactically, the Law of the Excluded Middle (LEM) is the axiom schema $P\lor\neg P$. Even in type theory, this would be something like $\Pi P:\mathsf{Prop}.P\lor (P\to\bot)$.

Externally, i.e. semantically (and particularly for categorical semantics), LEM means subobjects are complemented (or, particularly, subobjects of $1$ are). Propositions being "empty" or the "universe" sounds like semantic terminology. In type theory, $\top$ is simply the unit type having exactly one value. Calling it "the universe" doesn't make a lot of sense (and also conflicts with other uses of the term "universe" in type theory). Calling $\bot$ the "empty type" is reasonable enough, but calling it "empty" begins to suggest a little too much but isn't completely unreasonable. In the semantics of (single-sorted) first-order logic, people often talk about "true" (unary) predicates being interpreted as the "universe (of discourse)" or "domain" and "false" predicates being interpreted as the empty set. This "universe" terminology doesn't work that well even for multi-sorted first-order logic and is an even poorer fit (in this sense) for type theoretic work.

As a concrete example, $\mathbf{Set}\times\mathbf{Set}$ is a Boolean topos (so LEM holds) that is not two-valued. In particular, it has four truth values, $\bot=(0,0)$, $\top=(1,1)$, and also $(1,0)$ and $(0,1)$. All the operations are defined component-wise. You can easily show $P\lor\neg P$ and even $(P=\top)\lor(P=\bot)$ are valid with respect to this semantics. The latter can internally be read as saying "every proposition is either $\bot$ or $\top$". Externally, if we assign the truth value $(1,0)$ to $P$, then we're asking for the truth value of $(1,0)=(1,1)$ and $(1,0)=(0,0)$ which have the truth values $(1,0)$ and $(0,1)$ respectively. Of course, the join of these, i.e. the interperation of $\lor$, is $(1,1)$, i.e. the truth value of $\top$ as LEM requires.

Diaconescu's proof (which is only three pages long!) is talking about toposes, i.e. categorical semantics for constructive set theories. Unsurprisingly, it focuses on complemented subobjects.

$\neg\neg(P\lor\neg P)$ holds constructively. The only way to internally say "a proposition is neither empty nor the universe" in the way you appear to be using the words is to say something that is equivalent¹ to $\neg(P\lor\neg P)$, e.g. $\neg(P=\top)\land\neg(P=\bot)$, but this is contradictory in constructive logic itself even before we talk about LEM or the Axiom of Choice. Externally, we can easily say "if we have a subobject that's not complemented, then the Axiom of Choice does not hold" which is exactly what happens in Diaconescu's proof. If, however, you state (externally) that "if $0_1:0\rightarrowtail 1$ and $id_1:1\rightarrowtail 1$ aren't the only subobjects of $1$, then the Axiom of Choice does not hold" then this is just false. Any Boolean topos that is not two-valued, such as $\mathbf{Set}\times\mathbf{Set}$, would be a counter-example.

¹ In the presence of propositional extensionality which Diaconescu's theorem requires. Here's a formal proof in Agda that $\neg(P\equiv\top)\land\neg(P\equiv\bot)$ is contradictory:

data ⊥ : Set where

record ⊤ : Set where constructor tt

record _∧_ {ℓ}(A B : Set ℓ) : Set ℓ where
    constructor _,_
    field
        fst : A
        snd : B

¬ : ∀{ℓ} → Set ℓ → Set ℓ
¬ A = A → ⊥

data _≡_ {ℓ}{A : Set ℓ} (a : A) : A → Set ℓ where
    Refl : a ≡ a

isProp : Set → Set
isProp P = (x y : P) → x ≡ y

isProp-⊤ : isProp ⊤
isProp-⊤ tt tt = Refl

isProp-⊥ : isProp ⊥
isProp-⊥ () y

_↔_ : Set → Set → Set
P ↔ Q = (P → Q) ∧ (Q → P)

postulate propExt : {P Q : Set} → isProp P → isProp Q → (P ↔ Q) → P ≡ Q

thm1 : {P : Set} → isProp P → P → P ≡ ⊤
thm1 prf p = propExt prf isProp-⊤ ((λ _ → tt) , λ _ → p)

thm2 : {P : Set} → P ≡ ⊤ → P
thm2 Refl = tt

thm3 : {P : Set} → isProp P → ¬ P → P ≡ ⊥
thm3 prf ¬p = propExt prf isProp-⊥ (¬p , λ{ () })

thm4 : {P : Set} → P ≡ ⊥ → ¬ P
thm4 Refl p = p

thm5 : {P : Set} → isProp P → ¬ (P ≡ ⊤) ∧ ¬ (P ≡ ⊥) → ⊥
thm5 prf (¬P≡⊤ , ¬P≡⊥) with (λ p → ¬P≡⊤ (thm1 prf p)) | (λ ¬p → ¬P≡⊥ (thm3 prf ¬p))
... | ¬P | ¬¬P = ¬¬P ¬P