Teorema de Cantor na teoria dos tipos

9

O teorema de Cantor afirma que

Para qualquer conjunto A, o conjunto de todos os subconjuntos de A tem uma cardinalidade estritamente maior que o próprio A.

É possível codificar algo assim usando apenas tipos / proposições sem se referir a conjuntos ZFC? O código ou pseudocódigo para codificar essa proposição em uma linguagem tipicamente dependente seria apreciado.

Paula Vega
fonte

Respostas:

9

Resposta curta: sim! Você não precisa de tantas máquinas para obter a prova.

DddDdD

 para todas as declarações P,(P¬P)

Isso é suficiente, junto com a prova usual. Observe que, em geral, "rejeição" pode ter algumas nuances sutis na lógica construtiva / intuicionista (sem escolha);

Uma prova muito padrão no Coq (que por algum motivo não consegui encontrar on-line) pode ser a seguinte:

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.

Certamente, a estrutura "correta" na qual pensar sobre esses agrupamentos, que podem ser vistos como os requisitos mínimos para a prova, é o teorema do ponto fixo de Lawvere, que declara o que o teorema possui em todas as categorias fechadas cartesianas (portanto, em particular, em qualquer teoria razoável de tipos).

Andrej Bauer escreve lindamente sobre esse teorema no artigo Sobre teoremas de ponto fixo na computabilidade sintética , e suspeito que talvez haja algumas coisas interessantes a acrescentar a essa resposta.

cody
fonte
Se bem entendi, na sua definição de cantor, natdesempenha o papel de "qualquer conjunto A" e nat -> Propdesempenha o papel de "o conjunto de todos os subconjuntos de A". Quais seriam as implicações da substituição nat -> Propcom nat -> bool? Eu acho que usando Propé mais apropriado na lógica construtiva, mas a lógica clássica e teoria dos conjuntos muitas vezes assumem excluídos meio, por isso, devemos ser capazes de substituir Propcom boole ainda ser capaz de provar o teorema, certo?
Paula Vega
11
Sim, substituir Prop por bool funciona bem usando o mapa de negação. O teorema do ponto fixo de Lawvere mostra que você pode fazer isso com qualquer tipo A que tenha um mapa A -> A sem pontos fixos; portanto, um tipo com 3 elementos ou o tipo de todos os números naturais também funciona
Max New
@PaulaVega Max praticamente diz tudo, mas eu recomendo a brincar com o exemplo, por exemplo, usando boolem vez de Prope nate diag := fun b => negb (f b b), ou apenas substituir Propcom nate usar diag := fun n => (f b b) + 1.
Cody