Est-il possible de prouver l'indécidabilité du problème d'arrêt à Coq?

Je regardais les " Cinq étapes de l'acceptation des mathématiques constructives " d'Andrej Bauer et il dit qu'il y a deux types de preuves par contradiction (ou deux choses que les mathématiciens appellent preuve par contradiction):

1. Supposons que est faux ... bla bla bla, contradiction. Par conséquent, est vrai.$P$$P$
2. Supposons que soit vrai ... bla bla bla, contradiction. Par conséquent, est faux.$P$$P$

La première équivaut à la loi du milieu exclu (LEM) et la seconde consiste à prouver la négation.

La preuve de l'indécidabilité du problème de l'arrêt (HP) est une preuve par contradiction: supposons qu'il existe une machine qui puisse décider du HP ... bla bla bla, contradiction. Par conséquent, n'existe pas.$D$$D$

Donc, que soit " existe et peut décider du HP". Supposons que soit vrai ... bla bla bla, contradiction. Par conséquent, est faux.$P$$D$$P$$P$

Cela ressemble au deuxième type de preuve par contradiction, est-il donc possible de prouver l'indécidabilité du problème d'arrêt dans Coq (sans supposer LEM)?

EDIT: Je voudrais voir quelques points sur la preuve de cela en utilisant la contradiction. Je sais que cela peut également être prouvé en utilisant la diagonalisation.

Vous avez tout à fait raison de dire que le problème de l'arrêt est un exemple du deuxième type de «preuve par contradiction» - ce n'est vraiment qu'une déclaration négative.

Supposons decides_halt(M)qu'un prédicat indique que la machine Mdécide si son entrée est une machine qui s'arrête (c'est-à-dire, Mun programme qui, pour une machine met une entrée i, décide si elle ms'arrête en entrée i).

Oubliant un instant comment le prouver, le problème d'arrêt est la déclaration selon laquelle il n'y a pas de machine qui décide du problème d'arrêt. Nous pourrions déclarer cela dans Coq comme (exists M, decides_halt M) -> False, ou peut-être préférons-nous dire qu'une machine donnée ne résout pas le problème d'arrêt forall M, decides_halt M -> False. Il s'avère que sans aucun axiome ces deux formalisations sont équivalentes en Coq. (J'ai énoncé la preuve pour que vous puissiez voir comment cela fonctionne, mais vous firstorderferez tout cela!)

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.

Je pense que l'une ou l'autre de ces affirmations n'est pas trop difficile à prouver comme argument de diagonalisation, bien que formaliser les machines, la calculabilité et l'arrêt soit probablement assez difficile. Pour un exemple plus simple, il est pas trop difficile de prouver le théorème de diagonalisation de Cantor (voir https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 pour une preuve nat -> natet natne sont pas isomorphes).

La diagonalisation ci-dessus donne un exemple de la façon dont vous pourriez procéder pour dériver une contradiction d'un isomorphisme entre nat -> natet nat. Voici l'essence de cette preuve présentée comme un exemple autonome:

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.

Même sans regarder les détails, nous pouvons voir dans la déclaration que cette preuve prend la simple existence d'une bijection et démontre qu'elle est impossible. Nous donnons d'abord les deux côtés de la bijection les noms seqet index. La clé est que le comportement de la bijection à la séquence spéciale f := fun n => S (seq n n)et son indice index fsont contradictoires. La preuve du problème d'arrêt dériverait d'une contradiction de manière similaire, instanciant son hypothèse sur une machine qui résout le problème d'arrêt avec une machine soigneusement choisie (et en particulier une qui dépend en fait de la machine supposée).