Cantor's theorem in type theory

Question

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.

Answer 1

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.
Proof.
  intros P H; apply H.
    - apply <- H.
      intro p.
      apply H; exact p.
    - apply <- H; intro p; apply H; exact p.
Qed.


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

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.