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?

  • 1
    $\begingroup$ My intuition is that the axiom of separation (a.k.a. specification or comprehension) is at fault: if $P$ is not constructive, then the existence of $\{x : P\}$ is unclear - even in the case when $x$ does not appear free in $P$. What you call a "cheap trick" is putting this idea to work to show that separation, excluded middle and choice together lead to a contradiction. $\endgroup$ – Rob Arthan Nov 27 '18 at 19:12
  • $\begingroup$ @RobArthan I don't follow -- where's the contradiction? $\endgroup$ – Abhimanyu Pallavi Sudhir Nov 27 '18 at 19:55
  • 3
    $\begingroup$ The Law of the Excluded Middle does not state that "all propositions are either empty or the universe". It only states, using similarly analogical wording (and combined with the Law of Non-contradiction), that "every proposition and its negation partitions the universe". More precisely, it semantically means that every subobject is complemented. There are more Boolean algebras than just the two-element Boolean algebra. $\endgroup$ – Derek Elkins Nov 27 '18 at 20:02
  • $\begingroup$ The intuition (which is what you were asking for) is that the axiom of separation is very suspicious from a constructive perspective: how can I constructively form a subset defined by a non-constructive predicate? In my comment "excluded middle" was meant to read "the negation of the excluded middle" (i.e., I was referring to Diaconescu's argument) - apologies for any confusion. $\endgroup$ – Rob Arthan Nov 27 '18 at 20:23
  • $\begingroup$ @DerekElkins "All propositions are either empty or the universe" is exactly what the excluded middle states in type theory, where propositions are types containing their proofs. So "true" is the universal type (everything implies it/there is a function from any type to it) and "false" is the empty type (there is a function from it to every type), so the law of the excluded middle states "every statement is either true (the universal type) or false (the null type)". $\endgroup$ – Abhimanyu Pallavi Sudhir Nov 28 '18 at 10:54

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 equivalent1 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.

1 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 _,_
        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
  • $\begingroup$ $\top$ is often referred to as 'the universal type' and apparently (?) usually every object is of that type en.wikipedia.org/wiki/Top_type . My experience from the limited amount I've learned about this subject agrees with what you say, that $\top$ is a unit type with exactly one inhabitant (). (I guess wikipedia is referring situations where there is subtyping?) $\endgroup$ – spaceisdarkgreen Dec 1 '18 at 19:08
  • $\begingroup$ Anyway, I think although I learned a lot from this and it's dead on as far as I can tell, what might get lost in the details here is a succinct statement of what is wrong with OP's last comment: The colloquial statement 'classical means everything is either true or false' is being taken way too literally. $A\to B$ is not the same sentence as $\top$ or the same sentence as $\bot$ even if the logic is classical. This is indeed a confusion of syntax with semantics (and a massive oversimplification of semantics), $\endgroup$ – spaceisdarkgreen Dec 1 '18 at 19:16
  • $\begingroup$ That article itself states and suggests that universal types and unit types are distinct in multiple ways. But, frankly, that article seems pretty confused. Nevertheless, as you say, using terminology this way is more common in systems with subtyping. Often for theoretical systems the top of the subtyping lattice is, in fact, isomorphic to the unit type, but that's because there's so little you can do with a value of the top type. Changing topics, I also learned something writing this as I had not seen van den Berg's paper, though I knew that Diaconescu's theorem required more than just ITT. $\endgroup$ – Derek Elkins Dec 1 '18 at 19:57
  • $\begingroup$ Ok, thanks, this is a great answer -- I understand now why my phrasing is careless, and why my attempt at building an intuition does not hold (you need the converse of the contrapositive too, since you pointed out that $\neg\neg(P\lor\neg P)$ is constructible, which isn't possible). But I'll leave the question open for now, because I'm still not sure if I really understand the answer to the question itself, which is the intuition behind Diaconescu's theorem. $\endgroup$ – Abhimanyu Pallavi Sudhir Dec 1 '18 at 22:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.