Czy istnieją programy, które nigdy się nie zatrzymują i nie mają dowodu braku wypowiedzenia?

Jak czarne dziury w informatyce. Możemy tylko wiedzieć, że istnieją, ale kiedy będziemy mieli jeden z nich, nigdy nie będziemy wiedzieć, że to jeden z nich.

halting-problem correctness-proof

— Otakar Molnár López
źródło

Podjęcie decyzji o rozwiązaniu problemu jest co najmniej tak samo trudne jak udowodnienie twierdzeń (biorąc pod uwagę twierdzenie

można po prostu napisać program , program kończy się wtedy i tylko wtedy, gdy twierdzenie jest prawdziwe). Jeśli nie byłoby takich programów, oznaczałoby to, że można udowodnić wszystkie twierdzenia, o których wiadomo, że są fałszywe.

T

$T$ if T is true then halt else loop forever

— Bakuriu

@Bakuriu: Jak byś pisał if T is true?

— ruakh

@ruakh: Tradycyjna metoda toFor each string S in the (countable) universe of possible strings: If S is a syntactically valid proof of T, halt.

— Quuxplusone,

@Quuxplusone: Cóż, tak, ale to nie wydaje się pasować do konstrukcji Bakuriu. . .

— ruakh

To interesujące, ale poza moją wiedzą. Czy możesz opracować, proszę?

— Evorlor,

Odpowiedzi:

Rzeczywiście istnieją takie programy. Aby to udowodnić, załóżmy wręcz przeciwnie, że dla każdej maszyny, która się nie zatrzymuje, istnieje dowód, że się nie zatrzymuje.

$s$ $s$

$M$ $x$

s := 0
while (True)
    test if machine M halts on input x in s steps
    look at all proofs of length s and see if they prove M doesn't halt on input x
    set s := s + 1

$M$ $x$ $s$

$M$ $x$ $s$ $M$

Mamy więc algorytm decydujący o problemie zatrzymania, który zawsze się kończy. Wiemy jednak, że to nie może istnieć, więc nasze założenie, że zawsze istnieje dowód, że nie można zatrzymać, musi być fałszywe.

— jmite
źródło

Myślę, że z tego wynika również słabsza forma twierdzenia o niekompletności Boga. Zasadniczo istnieją rzeczy, które są prawdziwe, ale których nie można udowodnić. To jeden z moich nowych ulubionych eksperymentów myślowych.

— Jake

Czy myślisz, że próba udowodnienia P = NP lub próba znalezienia nieparzystej liczby może być jednym z tych programów?

— Otakar Molnár López

Nie ma to większego sensu, ponieważ programy nie kończące się nie są dowodami ani liczbami, ale pomysł, do którego zmierzasz, został podniesiony. Niektórzy twierdzą, że PvsNP jest nie do udowodnienia

— Jake

@Jake Uważam, że część motywacji maszyn Turinga była czystszym wyrazem idei stojącej za twierdzeniem Godela.

— cpast

Dla bardziej konkretnego przykładu załóżmy, że teoria, której używamy do naszych dowodów, ma następujące (całkiem rozsądne, IMO) cechy:

Jest spójny ; to znaczy, nie może udowodnić sprzeczności.
Jego zestaw aksjomatów jest rekurencyjnie wyliczalny.
Jego dowody można zapisać jako skończone ciągi bitów.
Pytanie, czy dany ciąg koduje w nim dobrze uformowany i poprawny dowód, jest rozstrzygane algorytmicznie w skończonym czasie.
Jest wystarczająco ekspresyjny, aby przyznać dowód na drugie twierdzenie Gödela o drugiej niekompletności , które mówi, że nie może on udowodnić swojej spójności.

Przy tych założeniach następujący program nigdy się nie zatrzyma, ale nie można udowodnić (w ramach stosowanej przez nas teorii), że się nie zatrzyma:

let k := 0;
repeat:
    let k := k + 1;
    let s := binary expansion of k, excluding leading 1 bit;
while s does not encode a proof of a contradiction;
halt.

Kluczowym szczegółem tutaj jest pierwsze założenie powyżej, a mianowicie, że teoria, której używamy do naszych dowodów, jest spójna. Oczywiście musimy to założyć, aby nasze dowody były cokolwiek warte, ale drugie twierdzenie Gödela o niekompletności mówi, że dla jakiejkolwiek racjonalnie ekspresyjnej i skutecznie aksjatyzowanej teorii nie możemy tego faktycznie udowodnić (z wyjątkiem być może jakiejś innej teorii, której spójności wtedy trzeba założyć itp.).

— Ilmari Karonen
źródło