Respuesta corta: si! No necesita tanta maquinaria para obtener la prueba.
Una sutileza: parece que hay un uso del medio excluido: uno construye un conjunto y un número , y muestra que o que lleva a una contradicción . Pero hay un lema, cierto en la lógica intuicionista, que dice:rerere∈ Dre∉ D
para todas las declaraciones P, ( P⟺¬ P) ⇒ ⊥
Esto es suficiente, junto con la prueba habitual. Tenga en cuenta que, en general, la "sobreyección" puede tener algunos matices sutiles en la lógica constructiva / intuicionista (sin opción), por lo que debe hacerlo con "derecho invertible".
Una prueba muy estándar en Coq (que por alguna razón no pude encontrar en línea) podría ser la siguiente:
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.
Por supuesto, el marco "correcto" en el que pensar acerca de estos asuntos, que pueden verse como los requisitos mínimos para que esta prueba pase, es el teorema del punto fijo de Lawvere que establece que el teorema se mantiene en cada categoría cerrada cartesiana (así en particular, en cualquier teoría de tipo razonable).
Andrej Bauer escribe maravillosamente sobre este teorema en el documento Sobre teoremas de punto fijo en computabilidad sintética , y sospecho que podría tener algunas cosas interesantes para agregar a esta respuesta.
cantor
,nat
desempeña el papel de "cualquier conjunto A" ynat -> Prop
desempeña el papel de "el conjunto de todos los subconjuntos de A". ¿Cuáles serían las implicaciones de reemplazarnat -> Prop
connat -> bool
? Supongo usandoProp
es más apropiado en la lógica constructiva, pero la lógica clásica y la teoría de conjuntos a menudo asumen excluido medio, así que debemos ser capaces de reemplazarProp
conbool
y aún así ser capaz de demostrar el teorema, ¿verdad?bool
lugar deProp
ynat
ydiag := fun b => negb (f b b)
, o simplemente reemplazarProp
connat
y usardiag := fun n => (f b b) + 1
.