Resposta curta: sim! Você não precisa de tantas máquinas para obter a prova.
Ddd∈ Dd∉ D
para todas as afirmaçõ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.
cantor
,nat
desempenha o papel de "qualquer conjunto A" enat -> Prop
desempenha o papel de "o conjunto de todos os subconjuntos de A". Quais seriam as implicações da substituiçãonat -> Prop
comnat -> bool
? Eu acho que usandoProp
é 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 substituirProp
combool
e ainda ser capaz de provar o teorema, certo?bool
em vez deProp
enat
ediag := fun b => negb (f b b)
, ou apenas substituirProp
comnat
e usardiag := fun n => (f b b) + 1
.