Nie, nie przyznam, podobnie jak nie przyznam, że brak dowodu na istnienie duszy, albo krasnoludków, to żaden argument...
Nie mamy dowodu, że człowiek jest komputerem. Nie mamy dowodu, że człowiek nie jest komputerem. Zatem... człowiek jest komputerem. Imponujące.
Człowiek? Masz na myśli jakiś egzemplarz gatunku Homo Sapiens?
Mam na myśli egzemplarz Homo Sapiens z kwantyfikatorem szczegółowym.
Spróbuj przybliżyć, które klasy problemów są według Ciebie rozwiązywalne dla (jakiegoś) człowieka.
Nierozstrzygalne? To w takim razie czego dotyczy "On Computable Numbers, with an Application to the Entscheidungsproblem" Turinga?
Turing zdefiniował w niej maszynę Turinga. Nie wiem, co Twoja wypowiedź ma wspólnego z tematem.
Udowodnienie, czy dany system formalny (albo maszyna z określonymi operacjami - jeśli wolisz) jest rozstrzygalny, jest samo w sobie nierozstrzygalne.
Albo pierwsze, albo drugie, albo Twoje przekonanie będzie błędne, co w końcu sam odkryjesz.
Nie mogę mieć możliwości sprawdzenia, że moje przekonanie będzie błędne. Gdybym miał, to mógłbym postawić tezę "podstawienie x jest rozwiązaniem równania y", sprawdzić, czy się mylę, wziąć następne podstawienie, sprawdzić i tak dalej.
Jedyną możliwością będzie, że odkryjemy problem, na którym wszyscy się "zawiesimy".
Zacznij od 'Metamathematics, Machines, and Goedel's Proof' Shankara.
Podaj jakiś link do tej publikacji, ew. zacytuj fragment, który mówi, że komputery potrafią udowodnić twierdzenie Goedla.
NQTHM dowodzi twierdzenia poprzez zastosowanie logicznych reguł wynikania.
Nie wierzę. Musisz potwierdzić tą tezę.
To, że człowiek go programuje, nie ma żadnego znaczenia dla naszej dyskusji
Nie chodzi mi o to, że człowiek go stworzył i puścił w ruch. Człowiek musi uczestniczyć w działaniu algorytmu (nie tylko jako heurystyka). Komputer sam nie będzie tego umiał.
Dobra, zupełnie już nie rozumiem, co masz na myśli pisząc "Konstruowanie zdań Goedla również jest nierozstrzygalne". Z tego co pamiętam, dowód Goedla był jak najbardziej konstruktywny, i pokazywał jak stworzyć G...
Masz do dyspozycji symbole arytmetyki - dodawanie, mnożenie, liczby, kwantyfikatory itp.
Daję Ci układ aksjomatów.
Zadanie: skonstruuj zdanie Goedla dla tego układu, ewentualnie odpowiedz, że takiego nie ma.
Hmmm... może tak: dla systemu formalnego S, zdanie G ma postać: "G nie da się udowodnić w S".
Eeee tam. Ja mogę Ci na ekranie napisać literki: "ZDANIE GOEDLA". Ułóż zdanie Goedla z symboli arytmetyki.
Potrafisz napisać program spełniający _każdą_ specyfikację? Jesteś pewien?
Każdą, której realizacja jest maszyną Turinga. Nie jestem pewien, ale jestem niemal bliski pewności. Jeszcze nie spotkałem takiego problemu rozstrzygalnego, którego któryś z ludzi nie umiałby zaprogramować.
h: Jeżeli umiesz, to opisz z grubsza, jak te algorytmy udowodniły twierdzenie Goedla. Bo ja potrafię pokazać, że jeżeli potrafią je udowodnić, to potrafią także rozwiązać problem stopu.
N: No to pokaż...
No cóż. Najpierw kodujemy jakoś arytmetykę w liczbach. Każdej formule przypisujemy liczbę naturalną. Przypisujemy również liczbę każdej teorii. Interesują nas wyłącznie teorie zbudowane z symboli arytmetyki - dodawania, liczb, kwantyfikatorów itp. Skoro każdej formule umiemy przyporządkować liczbę, to możemy wziąć formułę będącą koniunkcją wszystkich aksjomatów i wziąć jej numer. Właśnie tak będziemy numerować teorie.
Będziemy też mówić, że każda teoria ma tylko jeden aksjomat - w innych okolicznościach na to zdanie powiedzielibyśmy "koniunkcja wszystkich aksjomatów". Na przyszłość ograniczymy się również tylko do teorii zawierających arytmetykę - to znaczy takich, których aksjomat jest koniunkcją aksjmatu arytmetyki z jakimś dodatkowym zdaniem.
Twierdzenie Goedla mówi, że każda teoria zawierająca arytmetykę jest niezupełna albo sprzeczna. Istnieje zdanie zbudowane ze zwyczajnych symboli arytmetyki - dodawania, liczb, kwantyfikatorów itp., którego nie da się udowodnić przy pomocy aksjomatu naszej teorii (zawierającego aksjomat arytmetyki), a jednak jest prawdziwe. Ewentualnie cała teoria jest sprzeczna, wtedy każde zdanie jest jednocześnie prawdziwe i fałszywe, zatem teoria jest zupełna (tylko nic z tego nie mamy :) ).
Oznaczmy jakąś teorię zawierającą arytmetykę literą S. Zdanie "teoria S jest niezupełna lub sprzeczna" oznaczmy symbolem G(S). Zatem zdanie \forall(S){G(S)} będzie twierdzeniem Goedla. Jeżeli umiemy udowodnić twierdzenie Goedla, to umiemy także udowodnić każde ze zdań G(S). Aby udowodnić zdanie G(S) musimy pokazać albo, że teoria S jest niezupełna albo, że jest sprzeczna.
Rozważamy maszyny Turinga biorące jedną zmienną.
Każdemu stanowi chwilowemu maszyny Turinga (stan głowicy + pozycja głowicy + zawartość taśmy) przyporządkowujemy liczbę naturalną. Przyjmujemy następujące konwencje:
1. Stanowi "stop" przyporządkowujemy liczbę 0.
2. Jeżeli chcemy podać maszynie Turinga na wejściu liczbę n, to kodujemy stan początkowy jako 2 do potęgi n.
3. Każda liczba nie będąca zerem ani potęgą dwójki reprezentuje jakiś stan taśmy nie początkowy ani nie końcowy.
Każdej maszynie Turinga przyporządkowujemy funkcję jednej zmiennej, która bierze dany stan chwilowy i produkuje następny, zgodnie z funkcją przejścia tej maszyny. Każdej funkcji jednej zmiennej przyporządkowujemy jednoznacznie jakąś liczbę.
Twierdzisz, że istnieje algorytm, który potrafi udowodnić twierdzenie Goedla. OK, bierzemy taki algorytm. Nasz algorytm ma za zadanie dla podanej teorii S stwierdzić, czy jest ona sprzeczna, czy zupełna. Jeżeli Twój algorytm potrafi udowodnić twierdzenie Goedla dla każdego S, to tym bardziej umie to zrobić dla konkretnego S. Bierzemy dowód, który Twój algorytm zwrócił jako wynik i sprawdzamy, czy nasza teoria okazała się niezupełna, czy sprzeczna. Jeżeli jest sprzeczna, to w Twoim dowodzie znajdzie się negacja aksjomatu naszej teorii. Jeżeli niezupełna, to zapewne zdanie Goedla, ale to nieistotne. Umiemy dzięki Twojemu algorytmowi odróżnić teorie niezupełne od sprzecznych.
Tworzymy maszynę Turinga (jednej zmiennej), która działa następująco:
1. Wczytuje z wejścia liczbę n.
2. Tworzy zdanie: "Istnieje takie k, że k razy złożona ze sobą funkcja nr n od argumentu n jest równa 0".
3. Tworzymy aksjomat nowej teorii, będący koniunkcją aksjomatu arytmetyki oraz zdania utworzonego w punkcie 2.
4. Podajemy tę teorię Twojemu algorytmowi.
5. Jeżeli Twój algorytm stwierdził, że teoria jest sprzeczna, zwracamy 0. Jeżeli niezupełna, zwracamy 1.
Jeżeli podamy na wejście tego algorytmu liczbę n będącą reprezentacją funkcji symulującej maszynę Turinga, to odpowie on, czy maszyna ta zatrzyma się na swoim własnym numerze.
Jeżeli maszyna n zatrzymuje się na numerze n, to na pewno istnieje takie k, że funkcja o numerze n złożona ze sobą k razy na argumencie n będzie równa 0. Zatem dołączenie tego prawdziwego zdania (tworzonego w punkcie 2) do aksjomatu arytmetyki nie stworzy teorii sprzecznej. Stworzy teorię niezupełną, co pokaże Twój algorytm.
Jeżeli maszyna n nie zatrzymuje się na swoim własnym numerze, to zdanie "Istnieje takie k, że k razy złożona ze sobą funkcja nr n od argumentu n jest równa 0" będzie fałszywe. Dołączenie go do aksjomatu arytmetyki stworzy teorię sprzeczną.
Czyli istnienie algorytmu znajdującego dowód twierdzenia Goedla implikuje istnienie algorytmu rozwiązującego problem stopu.
Co należało udowodnić.
