¿Es posible demostrar la indecidibilidad del problema de detención en Coq?

Estaba viendo las " Cinco etapas de aceptar las matemáticas constructivas " de Andrej Bauer y dice que hay dos tipos de prueba por contradicción (o dos cosas que los matemáticos llaman prueba por contradicción):

1. Suponga que es falso ... bla, bla, bla, contradicción. Por lo tanto, es cierto.$P$$P$
2. Suponga que es cierto ... bla, bla, bla, contradicción. Por lo tanto, es falso.$P$$P$

El primero es equivalente a la Ley del Medio Excluido (LEM) y el segundo es cómo demostrar la negación.

La prueba de la indecidibilidad del Problema de detención (HP) es una prueba por contradicción: suponga que hay una máquina que puede decidir el HP ... bla, bla, bla, contradicción. Por lo tanto, no existe.$D$$D$

Entonces, que sea ​​" existe y puede decidir el HP". Suponga que es cierto ... bla, bla, bla, contradicción. Por lo tanto, es falso.$P$$D$$P$$P$

Este parece ser el segundo tipo de prueba por contradicción, ¿entonces es posible demostrar la indecidibilidad del problema de detención en Coq (sin asumir LEM)?

EDITAR: Me gustaría ver algunos puntos sobre probar esto usando la contradicción. Sé que esto también se puede probar utilizando la diagonalización.

Tiene toda la razón en que el problema de detención es un ejemplo del segundo tipo de "prueba por contradicción": en realidad es solo una afirmación negativa.

Supongamos que decides_halt(M)es un predicado que dice que la máquina Mdecide si su entrada es una máquina que se detiene (es decir, Mes un programa que para alguna máquina my entrada i, decide si se mdetiene en la entrada i).

Olvidando por un momento cómo probarlo, el problema de detención es la afirmación de que no hay máquina que decida el problema de detención. Podríamos decir esto en Coq como (exists M, decides_halt M) -> False, o tal vez preferimos decir que cualquier máquina no resuelve el problema de detención forall M, decides_halt M -> False. Resulta que sin ningún axioma estas dos formalizaciones son equivalentes en Coq. (He explicado la prueba para que pueda ver cómo funciona, ¡pero firstorderlo hará todo!)

Parameter machine:Type.
Parameter decides_halt : machine -> Prop.

(* Here are two ways to phrase the halting problem: *)

Definition halting_problem : Prop :=
  (exists M, decides_halt M) -> False.

Definition halting_problem' : Prop :=
  forall M, decides_halt M -> False.

Theorem statements_equivalent :
  halting_problem <-> halting_problem'.
Proof.
  unfold halting_problem, halting_problem'; split; intros.
  - exact (H (ex_intro decides_halt M H0)).
  - destruct H0.
    exact (H x H0).
Qed.

Creo que cualquiera de las afirmaciones no es demasiado difícil de demostrar como un argumento de diagonalización, aunque formalizar máquinas, la computabilidad y la detención probablemente sea un desafío razonable. Para un ejemplo más simple, no es demasiado difícil de demostrar el teorema de diagonalización de Cantor (ver https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 para una prueba de que nat -> naty natno son isomorfos).

La diagonalización anterior da un ejemplo de cómo se podría derivar una contradicción de un isomorfismo entre nat -> naty nat. Aquí está la esencia de esa prueba en línea como un ejemplo autónomo:

Record bijection A B :=
  {  to   : A -> B
  ; from : B -> A
  ; to_from : forall b, to (from b) = b
  ; from_to : forall a, from (to a) = a
  }.

Theorem cantor :
  bijection nat (nat -> nat) ->
  False.
Proof.
  destruct 1 as [seq index ? ?].
  (* define a function which differs from the nth sequence at the nth index *)
  pose (f := fun n => S (seq n n)).
  (* prove f differs from every sequence *)
  assert (forall n, f <> seq n). {
    unfold not; intros.
    assert (f n = seq n n) by congruence.
    subst f; cbn in H0.
    eapply n_Sn; eauto.
  }
  rewrite <- (to_from0 f) in H.
  apply (H (index f)).
  reflexivity.
Qed.

Incluso sin mirar los detalles, podemos ver en la declaración que esta prueba toma la mera existencia de una biyección y demuestra que es imposible. Primero le damos a los dos lados de la biyección los nombres seqy index. La clave es que el comportamiento de la biyección en la secuencia especial f := fun n => S (seq n n)y su índice index fes contradictorio. La prueba del problema de detención derivaría una contradicción de una manera similar, instanciando su hipótesis sobre una máquina que resuelve el problema de detención con una máquina cuidadosamente elegida (y en particular una que realmente depende de la máquina supuesta).