Apakah mungkin untuk membuktikan keraguan tentang masalah penghentian dalam Coq?

Saya menonton " Lima Tahapan Menerima Matematika Konstruktif " oleh Andrej Bauer dan dia mengatakan bahwa ada dua jenis pembuktian dengan kontradiksi (atau dua hal yang oleh para ahli matematika disebut pembuktian oleh kontradiksi):

1. Anggap salah ... bla bla bla, kontradiksi. Karena itu P benar.$P$$P$
2. Anggap benar ... bla bla bla, kontradiksi. Karena itu P salah.$P$$P$

Yang pertama setara dengan Law of Excluded Middle (LEM) dan yang kedua adalah bagaimana membuktikan negasi.

Bukti ketidakpastian Masalah Hentikan (HP) adalah bukti berdasarkan kontradiksi: anggap ada mesin yang dapat memutuskan HP ... bla bla bla, kontradiksi. Karenanya D tidak ada.$D$$D$

Jadi, biarkan menjadi " D ada dan dapat memutuskan HP". Anggap P benar ... bla bla bla, kontradiksi. Karena itu P salah.$P$$D$$P$$P$

Ini sepertinya adalah jenis bukti kedua berdasarkan kontradiksi, jadi mungkinkah untuk membuktikan ketidakpastian masalah penghentian dalam Coq (tanpa mengasumsikan LEM)?

EDIT: Saya ingin melihat beberapa poin tentang membuktikan ini menggunakan kontradiksi. Saya tahu bahwa ini juga dapat dibuktikan menggunakan diagonalisasi.

Anda benar bahwa masalah penghentian adalah contoh dari jenis kedua "bukti oleh kontradiksi" - itu benar-benar hanya pernyataan negatif.

Misalkan decides_halt(M)adalah predikat yang mengatakan bahwa mesin Mmemutuskan apakah inputnya adalah mesin yang berhenti (yaitu, Mprogram yang untuk beberapa mesin mdan input i, memutuskan apakah mberhenti pada input i).

Lupa sejenak tentang bagaimana membuktikannya, masalah penghentian adalah pernyataan bahwa tidak ada mesin yang memutuskan masalah penghentian. Kami mungkin menyatakan ini dalam Coq sebagai (exists M, decides_halt M) -> False, atau mungkin kami lebih suka mengatakan mesin yang diberikan tidak menyelesaikan masalah penghentian forall M, decides_halt M -> False. Ternyata tanpa aksioma, dua formalisasi ini setara dalam Coq. (Saya sudah menguraikan buktinya sehingga Anda dapat melihat cara kerjanya, tetapi firstorderakan melakukan semuanya!)

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.

Saya pikir kedua pernyataan itu tidak terlalu sulit untuk dibuktikan sebagai argumen diagonalisasi, meskipun memformalkan mesin, komputabilitas, dan penghentian mungkin cukup menantang. Sebagai contoh yang lebih sederhana, tidak terlalu sulit untuk membuktikan teorema diagonalisasi Cantor (lihat https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 untuk bukti bahwa nat -> natdan natbukan isomorfik).

Diagonalisasi di atas memberikan contoh bagaimana Anda bisa mendapatkan kontradiksi dari isomorfisme antara nat -> natdan nat. Inilah inti dari bukti yang diuraikan sebagai contoh yang lengkap:

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.

Bahkan tanpa melihat perinciannya, kita dapat melihat dari pernyataan bahwa bukti ini mengambil keberadaan belaka dan menunjukkan bahwa itu mustahil. Pertama-tama kita memberi dua sisi nama seqdan nama index. Kuncinya adalah bahwa perilaku bijih pada urutan khusus f := fun n => S (seq n n)dan indeksnya index fbertentangan. Bukti masalah terputus-putus akan menghasilkan kontradiksi dengan cara yang sama, membuat hipotesis tentang mesin yang menyelesaikan masalah penghentian dengan mesin yang dipilih dengan hati-hati (dan khususnya yang benar-benar tergantung pada mesin yang diasumsikan).