Cantor's theorem states that

For any set A, the set of all subsets of A has a strictly greater cardinality than A itself.

Is it possible to encode something like this using only types / propositions without referring to ZFC sets? Code or pseudocode for encoding this proposition in a dependently typed language would be appreciated.


Short answer: yes! You don't need that much machinery to get the proof to go through.

One subtlety: it seems on the face of it that there is a use of the excluded middle: one builds a set $D$ and a number $d$, and shows that either $d\in D$ or $d\not\in D$ which leads to a contradiction. But there is a lemma, true in intuitionistic logic, that states:

$$ \mbox{ for all statements } P, (P\iff \neg P) \Rightarrow \bot$$

This suffices, along with the usual proof. Note that in general "surjection" may have some subtle nuance in constructive/intuitionistic logic (without choice) so you have to make due with "right invertible" instead.

A very standard proof in Coq (which for some reason I couldn't find online) might go as follows:

Inductive right_invertible {A B:Type}(f : A->B):Prop :=
| inverse: forall g, (forall b:B, f (g b) = b) -> right_invertible f.

Lemma case_to_false :  forall P : Prop, (P <-> ~P) -> False.
  intros P H; apply H.
    - apply <- H.
      intro p.
      apply H; exact p.
    - apply <- H; intro p; apply H; exact p.

Theorem cantor :  forall f : nat -> (nat -> Prop), ~right_invertible f.
  intros f inv.
  destruct inv.
  pose (diag := fun n => ~ (f n n)).
  apply case_to_false with (diag (g diag)).
  - intro I; unfold diag in I.
    rewrite H in I. auto.
  - intro nI.
    unfold diag. rewrite H. auto.

Of course, the "right" framework in which to think about these maters, which can be seen as the minimal requirements for this proof to go through, is Lawvere's fixed point theorem which states the the theorem holds in every Cartesian Closed Category (so in particular, in any reasonable type theory).

Andrej Bauer writes beautifully about this theorem in the paper On fixed-point theorems in synthetic computability, and I suspect might have some interesting things to add to this answer.

  • $\begingroup$ If I understand correctly, in your definition of cantor, nat plays the role of "any set A" and nat -> Prop plays the role of "the set of all subsets of A". What would be the implications of replacing nat -> Prop with nat -> bool? I guess using Prop is more appropriate in constructive logic, but classical logic and set theory often assume excluded middle, so we should be able to replace Prop with bool and still be able to prove the theorem, right? $\endgroup$ – Paula Vega Feb 9 '18 at 4:20
  • 1
    $\begingroup$ Yes, replacing Prop with bool works fine using the negation map. Lawvere's fixed point theorem shows you can do it with any type A that has a map A -> A with no fixed points, so a type with 3 elements or type of all natural numbers also work $\endgroup$ – Max New Feb 9 '18 at 12:09
  • $\begingroup$ @PaulaVega Max pretty much says it all, but I recommend playing around with the example, e.g. using bool instead of Prop and nat and diag := fun b => negb (f b b), or just replacing Prop with nat and using diag := fun n => (f b b) + 1. $\endgroup$ – cody Feb 9 '18 at 13:20

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.