Théorème de Cantor en théorie des types

Le théorème de Cantor déclare que

Pour tout ensemble A, l'ensemble de tous les sous-ensembles de A a une cardinalité strictement supérieure à A lui-même.

Est-il possible d'encoder quelque chose comme ça en utilisant uniquement des types / propositions sans se référer aux ensembles ZFC? Un code ou un pseudocode pour coder cette proposition dans un langage typé de manière dépendante serait apprécié.

Réponse courte: oui! Vous n'avez pas besoin de beaucoup de machines pour obtenir la preuve.

Une subtilité: il semble à première vue qu'il y ait une utilisation du milieu exclu: on construit un ensemble et un nombre d , et montre que soit d ∈ D ou d ∉ D ce qui conduit à une contradiction. Mais il y a un lemme, vrai dans la logique intuitionniste, qui dit:$D$$d$$d\in D$$d\not\in D$

Cela suffit, avec la preuve habituelle. Notez qu'en général, la «surjection» peut avoir une nuance subtile dans la logique constructive / intuitionniste (sans choix), vous devez donc vous contenter de «juste inversible» à la place.

Une preuve très standard dans Coq (que pour une raison quelconque je n'ai pas pu trouver en ligne) pourrait se présenter comme suit:

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.

Bien sûr, le «bon» cadre dans lequel penser à ces matières, qui peut être considéré comme les exigences minimales pour que cette preuve passe, est le théorème de Lawvere à point fixe qui énonce le théorème tient dans chaque catégorie fermée cartésienne (donc dans notamment dans toute théorie de type raisonnable).

Andrej Bauer écrit magnifiquement à propos de ce théorème dans l'article sur les théorèmes à virgule fixe dans la calculabilité synthétique , et je soupçonne d'avoir des choses intéressantes à ajouter à cette réponse.