Twierdzenie Cantora w teorii typów

Twierdzenie Cantora stwierdza, że

Dla każdego zestawu A zbiór wszystkich podzbiorów A ma znacznie większą liczebność niż sam A.

Czy można zakodować coś takiego za pomocą typów / propozycji bez odwoływania się do zestawów ZFC? Doceniony zostanie kod lub pseudokod do kodowania tej propozycji w języku zależnym od typu.

Krótka odpowiedź: tak! Nie potrzebujesz tyle maszyn, aby przejść przez dowód.

Jedna subtelność: na pierwszy rzut oka wydaje się, że istnieje zastosowanie wykluczonego środka: buduje się zestaw i liczbę , i pokazuje, że albo albo co prowadzi do sprzeczności . Ale istnieje logika, prawdziwa w intuicyjnej logice, która stwierdza:$D$$d$$d\in D$$d\not\in D$

To wystarczy wraz ze zwykłym dowodem. Zauważ, że ogólnie „surjection” może mieć subtelny niuans w logice konstruktywnej / intuicyjnej (bez wyboru), więc zamiast tego musisz zrobić to z „prawą odwracalnością”.

Bardzo standardowy dowód w Coq (którego z jakiegoś powodu nie mogłem znaleźć w Internecie) może wyglądać następująco:

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.

Oczywiście „właściwą” ramą do myślenia o tych sprawach, którą można postrzegać jako minimalne wymagania, aby przejść przez ten dowód, jest twierdzenie o punkcie stałym Lawvere, które stwierdza, że ​​twierdzenie to utrzymuje się w każdej kartezjańskiej kategorii zamkniętej (więc w w szczególności w każdej rozsądnej teorii typów).

Andrej Bauer pięknie pisze o tym twierdzeniu w artykule na temat twierdzeń o punktach stałych w obliczeniach syntetycznych i podejrzewam, że może być kilka interesujących rzeczy do dodania do tej odpowiedzi.