Czy można udowodnić nierozstrzygalność problemu zatrzymania w Coq?

Oglądałem „ Pięć etapów akceptacji konstruktywnej matematyki ” Andreja Bauera i mówi on, że istnieją dwa rodzaje dowodów sprzeczności (lub dwie rzeczy, które matematycy nazywają dowodem sprzeczności):

1. Załóżmy, że jest fałszywe ... bla bla bla, sprzeczność. Dlatego jest prawdziwe.$P$$P$
2. Załóżmy, że jest prawdą ... bla bla bla, sprzeczność. Dlatego P jest fałszem.$P$$P$

Pierwszy jest równoważny Prawu Wykluczonego Środka (LEM), a drugi - jak udowodnić negację.

Dowód nierozstrzygalności problemu zatrzymania (HP) jest dowodem sprzeczności: załóżmy, że istnieje maszyna która może zadecydować o HP ... bla bla bla, sprzeczność. Dlatego D nie istnieje.$D$$D$

Niech więc będzie „ D istnieje i może decydować o HP”. Załóżmy, że P jest prawdą ... bla bla bla, sprzeczność. Dlatego P jest fałszem.$P$$D$$P$$P$

To wygląda na drugi rodzaj dowodu sprzeczności, więc czy można udowodnić nierozstrzygalność problemu zatrzymania w Coq (bez zakładania LEM)?

EDYCJA: Chciałbym zobaczyć kilka punktów na temat udowodnienia tego za pomocą sprzeczności. Wiem, że można to również udowodnić za pomocą diagonalizacji.

Masz całkowitą rację, że problem zatrzymania jest przykładem drugiego rodzaju „dowodu sprzeczności” - to tak naprawdę tylko negatywne stwierdzenie.

Załóżmy, że decides_halt(M)jest predykatem, który mówi, że maszyna Mdecyduje, czy jej wejście jest maszyną, która się zatrzymuje (to znaczy Mjest programem, który dla niektórych maszyn mi danych wejściowych idecyduje, czy mzatrzymuje się na wejściu i).

Zapominając na chwilę o tym, jak to udowodnić, problemem zatrzymania jest stwierdzenie, że nie ma maszyny, która rozstrzygałaby problem zatrzymania. Możemy to stwierdzić w Coq jako (exists M, decides_halt M) -> False, a może wolimy powiedzieć, że dana maszyna nie rozwiązuje problemu zatrzymania forall M, decides_halt M -> False. Okazuje się, że bez żadnych aksjomatów te dwie formalizacje są równoważne w Coq. (Podałem dowód, abyś mógł zobaczyć, jak to działa, ale firstorderzrobi wszystko!)

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.

Myślę, że którekolwiek z tych stwierdzeń nie jest zbyt trudne do udowodnienia jako argument przekątny, chociaż sformalizowanie maszyn, obliczalność i zatrzymanie jest prawdopodobnie dość trudne. Prostszy przykład, nie jest to zbyt trudne do udowodnienia diagonalizacja Twierdzenie Cantora (patrz https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 za dowód, że nat -> nati natnie są izomorficzne).

Powyższa diagonalizacja daje przykład, jak możesz dojść do sprzeczności z izomorfizmem pomiędzy nat -> nati nat. Oto istota tego dowodu przedstawiona jako samodzielny przykład:

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.

Nawet bez patrzenia na szczegóły możemy stwierdzić ze stwierdzenia, że ​​dowód ten zakłada jedynie istnienie bijectionu i pokazuje, że jest to niemożliwe. Najpierw nadamy obu stronom bijection nazwy seqi index. Kluczem jest to, że zachowanie bijectionu w specjalnej sekwencji f := fun n => S (seq n n)i jego indeksie index fjest sprzeczne. Dowód problemu zatrzymania mógłby doprowadzić do sprzeczności w podobny sposób, tworząc hipotezę o maszynie, która rozwiązuje problem zatrzymania za pomocą starannie wybranej maszyny (w szczególności takiej, która faktycznie zależy od założonej maszyny).