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):
- Załóżmy, że jest fałszywe ... bla bla bla, sprzeczność. Dlatego jest prawdziwe.
- Załóżmy, że jest prawdą ... bla bla bla, sprzeczność. Dlatego P jest fałszem.
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.
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.
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.
źródło
Odpowiedzi:
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 maszynaM
decyduje, czy jej wejście jest maszyną, która się zatrzymuje (to znaczyM
jest programem, który dla niektórych maszynm
i danych wejściowychi
decyduje, czym
zatrzymuje się na wejściui
).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 zatrzymaniaforall 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, alefirstorder
zrobi wszystko!)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 -> nat
inat
nie są izomorficzne).Powyższa diagonalizacja daje przykład, jak możesz dojść do sprzeczności z izomorfizmem pomiędzy
nat -> nat
inat
. Oto istota tego dowodu przedstawiona jako samodzielny przykład: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
seq
iindex
. Kluczem jest to, że zachowanie bijectionu w specjalnej sekwencjif := fun n => S (seq n n)
i jego indeksieindex f
jest 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).źródło