trawa

Autor Wątek: Człowiek a komputer  (Przeczytany 9792 razy)

0 użytkowników i 1 Gość przegląda ten wątek.

Offline haael

  • Starszy Gildii
  • *******
  • Wiadomości: 10 000
  • Total likes: 2
  • Płeć: Mężczyzna
  • Polska polska nie ciapolska.
Człowiek a komputer
« dnia: Lipiec 26, 2007, 11:28:39 am »
Witam szacownych forumowiczów.

Chciałbym zaproponować temat: w jakim stopniu procesy myślowe człowieka są powiązane z obliczeniami maszynowymi? Czy człowiek jest komputerem? Czy uda się kiedyś zrobić komputer obdarzony świadomością?

Za koronny dowód na to, że człowiek nie jest komputerem uważam ten przytoczony przez R. Penrose'a: człowiek potrafi rozwiązywać tzw. problemy nierozstrzygalne (IR) a komputer nie potrafi.
Istnieje kilka możliwych interpretacji tego faktu:
1. Człowiek posiada duszę, która mu to umożliwia.
2. Istnieje nieznany dziś proces fizyczny, który prowadzi do rozwiązywania takich problemów.
3. Człowiek wcale nie umie rozwiązywać problemów nierozstrzygalnych, tylko ma w mózgu wielką tablicę niektórych rozwiązań wpisanych na stałe.

Ja przychylam się do opcji nr... 1 :). Nie udowodniono istnienia procesów fizycznych rozwiązujących problemy IR. Nie udowodniono także ich nieistnienia, ale wydaje się to mało prawdopodobne.
Prepara tu palo en mano, que hay vienen los hombres malos.
Prepara tu palo hermano, que hay vienen los hombres malos.

Offline Sajuuk'

  • Szafarz bracki
  • *****
  • Wiadomości: 3 019
  • Total likes: 0
  • Płeć: Mężczyzna
  • z'; DROP TABLE profile; --
    • sireliah.com
Człowiek a komputer
« Odpowiedź #1 dnia: Lipiec 26, 2007, 11:01:34 pm »
Cytuj
1. Człowiek posiada duszę, która mu to umożliwia.


Czy człowiek, który nie rozwiąże takiego problemu nie ma duszy?

Brakuje jeszcze jednej opcji przy wyjaśnieniach dlaczego człowiek radzi sobie z problemem nierozstrzygalnym: może człowiek wcale nie wykazuje prawdziwości danego twierdzenia jak tego czy Maszyna Turinga zakończy kiedyś działania na liczbie m. Może tylko przyjmuje jakąś półprawdę, nie bierze pod uwagę jakiegoś czynnika, bądź upraszcza? Czegoś takiego cyfrowej maszynie logicznej nie wolno zrobić, jeśli nie jest zawarte w programie.
"Był to chłopak tak piękny, że nie musiał się nawet myć" - T. Konwicki, "Dziura w niebie"

Offline haael

  • Starszy Gildii
  • *******
  • Wiadomości: 10 000
  • Total likes: 2
  • Płeć: Mężczyzna
  • Polska polska nie ciapolska.
Człowiek a komputer
« Odpowiedź #2 dnia: Lipiec 27, 2007, 12:01:16 am »
Cytuj
Czy człowiek, który nie rozwiąże takiego problemu nie ma duszy?

Osobiście rzeczywiście sądzę, że tylko matematycy, którzy potrafią udowodnić twierdzenie Goedla, potwierdzili swoje człowieczeństwo :). Co do humanistów, nie byłbym tego taki pewnien :).

A na serio - człowiek posiada potencjalną zdolność rozwiązywania problemów IR. I to świadczy o tym, że nie jest komputerem, bo komputery takiej potencjalnej zdolności nie mają.

Cytuj
Brakuje jeszcze jednej opcji przy wyjaśnieniach dlaczego człowiek radzi sobie z problemem nierozstrzygalnym: może człowiek wcale nie wykazuje prawdziwości danego twierdzenia jak tego czy Maszyna Turinga zakończy kiedyś działania na liczbie m. Może tylko przyjmuje jakąś półprawdę, nie bierze pod uwagę jakiegoś czynnika, bądź upraszcza? Czegoś takiego cyfrowej maszynie logicznej nie wolno zrobić, jeśli nie jest zawarte w programie.

To się sprowadza do punktu trzeciego - człowiek wcale nie rozwiązuje problemów nierozstrzygalnych, tylko oszukuje. A jeżeli Twoim zdaniem owo rozważanie "półprawd" naprawdę prowadzi do ścisłego rozwiązania problemu stopu, to zmiatasz tylko sprawę pod dywan.

Albo da się przy pomocy skończonego zbioru reguł rozwiązać jakiś problem, albo się nie da. Tertium non datur. Komputer nie jest w stanie rozwiązać problemów IR. Człowiek owszem.

To jest właśnie ten punkt - człowiek ma w sobie jakąś nieskończoność. Mamy jakimś cudem dostęp do nieskończonej ilości informacji. Oczywiście można twierdzić, że tak naprawdę znamy tylko początek tej tablicy i kiedyś się nam ona skończy. Natrafimy wtedy na problemy, których nie będziemy umieli nigdy rozwiązać. Oczywiście są problemy, których do dzisiaj mimo setek lat prób nie złamaliśmy, ale historia pokazuje, że nie należy za szybko kłaść na ludziach krzyżyka.
Prepara tu palo en mano, que hay vienen los hombres malos.
Prepara tu palo hermano, que hay vienen los hombres malos.

Offline Scyzoryk

Człowiek a komputer
« Odpowiedź #3 dnia: Lipiec 27, 2007, 01:28:35 am »
Pewnie jestem ignorantem, ale co to są problemy nierostrzygalne?

Offline Neratin

Człowiek a komputer
« Odpowiedź #4 dnia: Lipiec 27, 2007, 09:52:20 am »
Cytat: "haael"
Chciałbym zaproponować temat: w jakim stopniu procesy myślowe człowieka są powiązane z obliczeniami maszynowymi? Czy człowiek jest komputerem? Czy uda się kiedyś zrobić komputer obdarzony świadomością?

Moim zdaniem odpowiedzi brzmią: całkowicie, tak, tak.

Cytuj

Za koronny dowód na to, że człowiek nie jest komputerem uważam ten przytoczony przez R. Penrose'a: człowiek potrafi rozwiązywać tzw. problemy nierozstrzygalne (IR) a komputer nie potrafi.

Czy potrafisz podać przykład problemu nierozstrzygalnego, który potrafi rozwiązać człowiek?

Bo jak dla mnie, dowód Penrose'a to tylko stary dowód Lucasa w nowym przebraniu. I posiada ten sam słaby punkt: to, że ja potrafię wypowiedzieć zdanie "Penrose nie potrafi w wypowiedzieć niniejszego zdania bez popadania w sprzeczność" bez popadania w sprzeczność, a Penrose nie, nie oznacza że nad nim góruję intelektualnie.

Cytuj

Osobiście rzeczywiście sądzę, że tylko matematycy, którzy potrafią udowodnić twierdzenie Goedla, potwierdzili swoje człowieczeństwo :). Co do humanistów, nie byłbym tego taki pewnien :).


No ale maszyny też potrafią udowodnić twierdzenie Goedla...

Cytuj
A na serio - człowiek posiada potencjalną zdolność rozwiązywania problemów IR. I to świadczy o tym, że nie jest komputerem, bo komputery takiej potencjalnej zdolności nie mają.

No ale teza, że człowiek potrafi rozwiązać problemy IR, jest niczym niepoparta...

Offline haael

  • Starszy Gildii
  • *******
  • Wiadomości: 10 000
  • Total likes: 2
  • Płeć: Mężczyzna
  • Polska polska nie ciapolska.
Człowiek a komputer
« Odpowiedź #5 dnia: Lipiec 27, 2007, 12:55:52 pm »
Cytuj
Pewnie jestem ignorantem, ale co to są problemy nierostrzygalne?

Takie problemy, których nie potrafi rozwiązać maszyna Turinga. Na mocy tezy Churcha, nie potrafi ich zatem rozwiązać żaden "automatyczny" lub "mechaniczny" proces.
Nie do końca wiadomo, jak zdefiniować "mechaniczność". Ludzie na ogół czują to intuicyjnie, ale nie potrafią tego zapisać na kartce.
Weźmy maszynę, która ma skończenie ale dowolnie dużo liczników, w których potrafi zapisywać dowolnie duże liczby. Może wykonywać na nich operacje: dodawania, odejmowania, mnożenia oraz porównywania. Taka maszyna jest w stu procentach mechaniczna i potrafi rozwiązywać problemy rozstrzygalne i nic poza tym.
Ale dorzućmy do tej maszyny jeszcze jeden operator. Zastosowanie tego operatora na liczbie przebiega następująco: liczba ta jest traktowana jako symboliczny zapis ("kod źródłowy") pewnej maszyny Turinga. Operator ten udziela odpowiedzi, czy owa maszyna zatrzyma się, czy nie i zwraca wartość 1 lub 0. Taki operator nazywa się wyrocznią. Maszyna weń wyposażona również jest całkowicie "mechaniczna", ale jednak intuicyjnie czujemy, że jest tu jakieś oszustwo.

Cytuj
Moim zdaniem odpowiedzi brzmią: całkowicie, tak, tak.

Czyli człowiek jest Twoim zdaniem komputerem. Powiedz mi wobec tego - czy nie czujesz, że istnienie świadomości jest sprzeczne z brzytwą Ockhama? Przecież natura mogła nas wyposażyć we wszystkie niezbędne algorytmy, umiejętność komunikacji, rozwiązywania problemów, a jednak dorzuciła "niepotrzebną" świadomość.
Trudno zdefiniować świadomość, ale chyba wszyscy rozumieją, o co chodzi. Świadomość to inaczej nasze "ja", ta część naszej psychiki, która sprawia, że wydaje się nam, że mamy duszę. Wyobraźcie sobie, że ktoś przeniósł Waszą świadomość do kamienia albo stołu, ale Wasz mózg nadal pracuje i robi wszystko mechanicznie, że ludzie nie widzą żadnej zmiany Waszego zachowania. To właśnie jest świadomość.
Po co Twoim zdaniem natura nam ją dała, skoro da się obejść bez niej?

Cytuj
Czy potrafisz podać przykład problemu nierozstrzygalnego, który potrafi rozwiązać człowiek?

Równania diofantyczne. Problem odpowiedniości Posta. Dowodzenie zgodności programu ze specyfkacją. Konstruowanie zdań Goedla.

Cytuj
Bo jak dla mnie, dowód Penrose'a to tylko stary dowód Lucasa w nowym przebraniu. I posiada ten sam słaby punkt: to, że ja potrafię wypowiedzieć zdanie "Penrose nie potrafi w wypowiedzieć niniejszego zdania bez popadania w sprzeczność" bez popadania w sprzeczność, a Penrose nie, nie oznacza że nad nim góruję intelektualnie.

Ależ udowodniono matematycznie, że maszyny Turinga są od nas głupsze. Maszyny Turinga potrafią rozwiązać tylko Alef 0 problemów, co więcej, istnieją konkretne problemy, których żadna taka maszyna nie rozwiąże.

Cytuj
No ale maszyny też potrafią udowodnić twierdzenie Goedla...

Słucham????? Zaskakujesz mnie. Absolutnie nie potrafią. Powiedz, co masz na myśli.

Cytuj
No ale teza, że człowiek potrafi rozwiązać problemy IR, jest niczym niepoparta...

Poparta doświadczeniem. Sam rozwiązałem niejeden problem IR, choćby pisząc program komputerowy, który dodaje dwa do dwóch.
Prepara tu palo en mano, que hay vienen los hombres malos.
Prepara tu palo hermano, que hay vienen los hombres malos.

Offline Neratin

Człowiek a komputer
« Odpowiedź #6 dnia: Lipiec 27, 2007, 01:30:45 pm »
Cytat: "haael"

Czyli człowiek jest Twoim zdaniem komputerem. Powiedz mi wobec tego - czy nie czujesz, że istnienie świadomości jest sprzeczne z brzytwą Ockhama?

Nie.

Cytuj
Przecież natura mogła nas wyposażyć we wszystkie niezbędne algorytmy, umiejętność komunikacji, rozwiązywania problemów, a jednak dorzuciła "niepotrzebną" świadomość.

Skąd wiesz, że niepotrzebną? Nie znamy adaptacyjnej funkcji świadomości.

Cytuj
Po co Twoim zdaniem natura nam ją dała, skoro da się obejść bez niej?

Nie wiem, po co. I nie wiem, czy da się obejść bez niej, tzn. czy odpowiednio złożone algorytmy nie są przypadkiem samoświadome.


Cytuj

Równania diofantyczne.

I jesteś pewien, że człowiek potrafi rozwiązać _każde_ równanie diofantyczne? Można wiedzieć, skąd czerpiesz tę wiedzę?

Cytuj

Problem odpowiedniości Posta. Dowodzenie zgodności programu ze specyfkacją. Konstruowanie zdań Goedla.

Jak wyżej... (z pominięciem ostatniego - bo konstruowanie zdań Goedla nie jest problemem nierozstrzygalnym).

Cytuj

Ależ udowodniono matematycznie, że maszyny Turinga są od nas głupsze.

Ależ nie, nikt tego nie udowodnił...

Cytuj
Maszyny Turinga potrafią rozwiązać tylko Alef 0 problemów, co więcej, istnieją konkretne problemy, których żadna taka maszyna nie rozwiąże.

Zgadza się. Problem jednak polega na tym, że nikt nie udowodnił, że człowiek też potrafi je rozwiązać...

Cytuj

Słucham????? Zaskakujesz mnie. Absolutnie nie potrafią. Powiedz, co masz na myśli.

Mam na myśli dokładnie to, co napisałem: komputery potrafią udowodnić twierdzenie Goedla (które najwyraźniej mylisz ze zdaniem Goedla). Dokładniej, mam na myśli automatyczne systemy dowodzące, takie jak NQTHM Boyera i Moora (algorytm Shankara z 1986, dla systemu aksjomatycznego Z2), albo Coq (algorytm O'Connora z 2005, dla arytmetyki Peano).

Cytuj

Poparta doświadczeniem. Sam rozwiązałem niejeden problem IR, choćby pisząc program komputerowy, który dodaje dwa do dwóch.

LOL!
Przecież zalgorytmizowanie czynności pisania programu, który dodaje dwa do dwóch, jest trywialne.

Offline haael

  • Starszy Gildii
  • *******
  • Wiadomości: 10 000
  • Total likes: 2
  • Płeć: Mężczyzna
  • Polska polska nie ciapolska.
Człowiek a komputer
« Odpowiedź #7 dnia: Lipiec 27, 2007, 02:09:31 pm »
Cytuj
I jesteś pewien, że człowiek potrafi rozwiązać _każde_ równanie diofantyczne? Można wiedzieć, skąd czerpiesz tę wiedzę?

Cytuj
Ależ nie, nikt tego nie udowodnił...

Cytuj
Zgadza się. Problem jednak polega na tym, że nikt nie udowodnił, że człowiek też potrafi je rozwiązać...

Odwołujesz się na razie do naszej zbiorowej niewiedzy. Nie udowodniliśmy, że człowiek potrafi rozwiązywać problemy nierozstrzygalne. Przyznasz jednak, że brak dowodu, to żaden argument.

Musimy na początek ustalić, co Twoim zdaniem umie człowiek. Nie udowodniono przecież nawet, że człowiek umie dodawać 1 do każdej liczby. Być może istnieje jakaś liczba, której nikt jeszcze nie odkrył, że żaden człowiek nie będzie umiał dodać do niej jedynki? Nie mamy dowodu, ale chyba się zgodzisz, że człowiek jednak doda 1 do każdej liczby. Powiedz więc, co Twoim zdaniem umie człowiek.

Aha, jeżeli człowiek nie umie rozwiązywać problemów nierozstrzygalnych, to nie umie także tego udowodnić. Bo udowodnienie, że jakaś maszyna umie lub nie umie rozwiązywać problemów IR, samo w sobie jest nierozstrzygalne.

Mam też pytanie: skoro nie umiem rozwiązywać np. równań diofantycznych, to jak wyobrażasz sobie sytuację, że w końcu moja niedoskonałość wyjdzie na jaw? Spotkam równanie, którego za nic nie będę umiał rozgryźć, czy też może będzie mi się wydawało, że je rozwiązałem, ale moje przekonanie będzie błędne (czego zresztą nie uda mi się nigdy udowodnić)?

Cytuj
Mam na myśli dokładnie to, co napisałem: komputery potrafią udowodnić twierdzenie Goedla (które najwyraźniej mylisz ze zdaniem Goedla). Dokładniej, mam na myśli automatyczne systemy dowodzące, takie jak NQTHM Boyera i Moora (algorytm Shankara z 1986, dla systemu aksjomatycznego Z2), albo Coq (algorytm O'Connora z 2005, dla arytmetyki Peano).

Zapodaj jakieś źródło Twojego twierdzenia. Z tego, co znalazłem w Internecie wynika, że użyto systemu NQTHM do sformalizowania dowodu twierdzenia Goedla, a nie do samego dowodzenia. Czyli ten system to raczej proof-asistant niż theorem-proover. To człowiek go programuje, a system dostarcza jedynie ładnych znaczków.

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.

Nie mylę zdania Goedla z twierdzeniem Goedla. Konstruowanie zdań Goedla również jest nierozstrzygalne. (Masz dany układ aksjomatów. Skonstruuj zdanie Goedla dla tego układu.)

Cytuj
LOL!
Przecież zalgorytmizowanie czynności pisania programu, który dodaje dwa do dwóch, jest trywialne.

To była figura retoryczna. Potrafię napisać program spełniający specyfikację. Pokaż mi algorytm, który zrobi to za mnie. Zarobię na nim sporo kasy.
Prepara tu palo en mano, que hay vienen los hombres malos.
Prepara tu palo hermano, que hay vienen los hombres malos.

Offline Neratin

Człowiek a komputer
« Odpowiedź #8 dnia: Lipiec 27, 2007, 10:03:16 pm »
Cytat: "haael"
Odwołujesz się na razie do naszej zbiorowej niewiedzy. Nie udowodniliśmy, że człowiek potrafi rozwiązywać problemy nierozstrzygalne.

Odwołuję się do Twojej tezy, że to zostało "matematycznie udowodnione". Co nie jest prawdą: teza u wyższości człowieka nad maszyną to tylko czcza spekulacja.

Cytuj
Przyznasz jednak, że brak dowodu, to żaden argument.

Nie, nie przyznam, podobnie jak nie przyznam, że brak dowodu na istnienie duszy, albo krasnoludków, to żaden argument...

Cytuj

Musimy na początek ustalić, co Twoim zdaniem umie człowiek. Nie udowodniono przecież nawet, że człowiek umie dodawać 1 do każdej liczby. Być może istnieje jakaś liczba, której nikt jeszcze nie odkrył, że żaden człowiek nie będzie umiał dodać do niej jedynki? Nie mamy dowodu, ale chyba się zgodzisz, że człowiek jednak doda 1 do każdej liczby. Powiedz więc, co Twoim zdaniem umie człowiek.


Człowiek? Masz na myśli jakiś egzemplarz gatunku Homo Sapiens?

Cytuj

Aha, jeżeli człowiek nie umie rozwiązywać problemów nierozstrzygalnych, to nie umie także tego udowodnić. Bo udowodnienie, że jakaś maszyna umie lub nie umie rozwiązywać problemów IR, samo w sobie jest nierozstrzygalne.


???

Nierozstrzygalne? To w takim razie czego dotyczy "On Computable Numbers, with an Application to the Entscheidungsproblem" Turinga?

Cytuj

Mam też pytanie: skoro nie umiem rozwiązywać np. równań diofantycznych, to jak wyobrażasz sobie sytuację, że w końcu moja niedoskonałość wyjdzie na jaw? Spotkam równanie, którego za nic nie będę umiał rozgryźć, czy też może będzie mi się wydawało, że je rozwiązałem, ale moje przekonanie będzie błędne (czego zresztą nie uda mi się nigdy udowodnić)?

Albo pierwsze, albo drugie, albo Twoje przekonanie będzie błędne, co w końcu sam odkryjesz.

Cytuj

Zapodaj jakieś źródło Twojego twierdzenia.

Zacznij od  'Metamathematics, Machines, and Goedel's Proof' Shankara.

Cytuj
Z tego, co znalazłem w Internecie wynika, że użyto systemu NQTHM do sformalizowania dowodu twierdzenia Goedla, a nie do samego dowodzenia. Czyli ten system to raczej proof-asistant niż theorem-proover. To człowiek go programuje, a system dostarcza jedynie ładnych znaczków. Jeżeli umiesz, to opisz z grubsza, jak te algorytmy udowodniły twierdzenie Goedla.

NQTHM dowodzi twierdzenia poprzez zastosowanie logicznych reguł wynikania. Oczywiście, by nie błądził po omacku (to znaczy, by znalazł dowód w sensownym czasie - bo jest chyba jasne, że działając w drugą stronę, komputer może wychodząc od aksjomatów wygenerować dowolny dowód, o ile istnieje - ich liczba jest przeliczalna), wyposaża się go w bazę danych zawierającą heurystyki umożliwiające wydajniejsze odwoływanie się do aksjomatów, reguł logicznych, definicji, lematów czy innych twierdzeń. To, że człowiek go programuje, nie ma żadnego znaczenia dla naszej dyskusji - w końcu nikt nie twierdzi, że SI powstanie spontanicznie, samo z siebie; z drugiej strony, zapodane przez człowieka heurystyki to też tylko 'ładne znaczki'.

Cytuj
Bo ja potrafię pokazać, że jeżeli potrafią je udowodnić, to potrafią także rozwiązać problem stopu.

No to pokaż...

Cytuj
Nie mylę zdania Goedla z twierdzeniem Goedla. Konstruowanie zdań Goedla również jest nierozstrzygalne.

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...
Cytuj
(Masz dany układ aksjomatów. Skonstruuj zdanie Goedla dla tego układu.)

Hmmm... może tak: dla systemu formalnego S, zdanie G ma postać: "G nie da się udowodnić w S".

Cytuj

To była figura retoryczna. Potrafię napisać program spełniający specyfikację. Pokaż mi algorytm, który zrobi to za mnie. Zarobię na nim sporo kasy.

Potrafisz napisać program spełniający _każdą_ specyfikację? Jesteś pewien?

Offline haael

  • Starszy Gildii
  • *******
  • Wiadomości: 10 000
  • Total likes: 2
  • Płeć: Mężczyzna
  • Polska polska nie ciapolska.
Człowiek a komputer
« Odpowiedź #9 dnia: Lipiec 28, 2007, 07:55:57 pm »
Cytuj
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.

Cytuj
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.

Cytuj
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.

Cytuj
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".

Cytuj
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.

Cytuj
NQTHM dowodzi twierdzenia poprzez zastosowanie logicznych reguł wynikania.

Nie wierzę. Musisz potwierdzić tą tezę.

Cytuj
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ł.

Cytuj
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.

Cytuj
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.

Cytuj
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ć.

Cytuj
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ć.
Prepara tu palo en mano, que hay vienen los hombres malos.
Prepara tu palo hermano, que hay vienen los hombres malos.

Offline Neratin

Człowiek a komputer
« Odpowiedź #10 dnia: Lipiec 29, 2007, 12:15:20 pm »
Cytat: "haael"
Nie mamy dowodu, że człowiek jest komputerem. Nie mamy dowodu, że człowiek nie jest komputerem. Zatem... człowiek jest komputerem. Imponujące.

No cóż, ja wyrażałem tylko swoje zdanie (wspierając je np. tym, że w ramach obowiązującej fizyki hiperobliczenia są niemożliwe). Natomiast to _Ty_ twierdziłeś, że udowodniono, iż człowiek nie jest komputerem. Co jest tyleż imponujące, co nieprawdziwe.

Cytuj
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.

Ze względów fizycznych i egzystencjonalnych, w przypadku człowieka nie można mówić o rozwiązywaniu całych klas problemów, tylko konkretnych ich instancji.

Cytuj

Turing zdefiniował w niej maszynę Turinga. Nie wiem, co Twoja wypowiedź ma wspólnego z tematem.

ROTFL. Napisałeś:

"Udowodnienie, że jakaś maszyna umie lub nie umie rozwiązywać problemów IR, samo w sobie jest nierozstrzygalne."

Co jest bzdurą (pomijam już kwestię, łagodnie mówiąc, braku precyzji sformułowania 'udowodnienie ... jest nierozstrzygalne'). Bo przecież w "On Computable Numbers, with an Application to the Entscheidungsproblem" Turing _udowodnił_, że maszyna nie umie rozwiązać pewnego typu problemu.

Cytuj

Udowodnienie, czy dany system formalny (albo maszyna z określonymi operacjami - jeśli wolisz) jest rozstrzygalny, jest samo w sobie nierozstrzygalne.

???

Co to znaczy, że system formalny jest rozstrzygalny?
Co to znaczy, że udowodnienie jest nierozstrzygalne?

Cytuj

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".

Nie możesz mieć możliwości sprawdzenia prawdziwości _każdego_ twierdzenia. Nic nie stoi natomiast na przeszkodzie, być mógł sprawdzić _niektóre_ z nich. Chyba nie wierzysz, że nie potrafisz znaleźć np. trywialnych błędów logicznych albo arytmetycznych...


Cytuj
Nie wierzę. Musisz potwierdzić tą tezę.

ROTFL! No ale co jest w tym kontrowersyjnego? Masz aksjomaty i reguły wynikania, więc generowanie dowodów to czynność typograficzna - zastępowanie jednych symboli innymi.

Cytuj
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ł.

No ale właśnie to, że człowiek w przypadku interaktywnych proverów bierze udział w procesie dowodzenia, nie wynika z tego, że komputer 'sam nie będzie tego umiał', tylko ze względów praktycznych: wygenerowanie formalnego dowodu może pochłonąć tyle zasobów obliczeniowych, że będzie niepraktyczne.

Cytuj

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.

Twierdzenie Goodsteina dla PA.

Cytuj

Eeee tam. Ja mogę Ci na ekranie napisać literki: "ZDANIE GOEDLA". Ułóż zdanie Goedla z symboli arytmetyki.

Technika numeracji Goedla też jest powszechnie znana...

Cytuj
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ć.

No ale my mówimy tu o problemach nierozstrzygalnych. Które, rzekomo, potrafisz rozwiązać - innymi słowy, dla każdej instancji takiego problemu potrawisz znaleźć rozwiązanie. Co jest trochę naiwne - to tak jakbyś napisał program analizujący składnię algorytmów np. pod kątem warunków pętli, przetestował go na kilkunastu przypadkach, po czym doszedł do wniosku, że Twój algorytm potrafi rozwiązać problem stopu.

Cytuj

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.

Ależ skąd. Czy aby rozstrzygnąć prawdziwość zdania (p)^(~p), musisz rozstrzygnąć, czy p jest prawdziwe, albo fałszywe? Czy znając dowód Goedla, potrafisz rozstrzygnąć, że np. ZFC jest niezupełna, czy też może jest sprzeczna?

Cytuj

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.

Mylisz się. Nasz algorytm ma za zadanie udowodnić twierdzenie Goedla, a nie decydować, czy podana teoria S jest sprzeczna, czy niezupełna...

Cytuj
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.

No ale dowód, który mój algorytm zwrócił jako wynik, nie powie Ci, czy Twoja teoria okazała się niezupełna, czy sprzeczna. Mój algorytm powie Ci tylko, że dowolna teoria zawierająca arytmetykę musi być albo sprzeczna, albo niezupełna...

Cytuj
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.

Nie, nie umiemy...

Cytuj

Czyli istnienie algorytmu znajdującego dowód twierdzenia Goedla implikuje istnienie algorytmu rozwiązującego problem stopu.
Co należało udowodnić.

No chyba nie bardzo...

Offline haael

  • Starszy Gildii
  • *******
  • Wiadomości: 10 000
  • Total likes: 2
  • Płeć: Mężczyzna
  • Polska polska nie ciapolska.
Człowiek a komputer
« Odpowiedź #11 dnia: Lipiec 29, 2007, 04:31:32 pm »
Cytuj
Ze względów fizycznych i egzystencjonalnych, w przypadku człowieka nie można mówić o rozwiązywaniu całych klas problemów, tylko konkretnych ich instancji.

Z komputerem jest tak samo. On też nie oblicza wszystkich instancji problemu, tylko niektóre, dopóki mu prądu nie wyłączą.

Cytuj
ROTFL. Napisałeś:

"Udowodnienie, że jakaś maszyna umie lub nie umie rozwiązywać problemów IR, samo w sobie jest nierozstrzygalne."

Co jest bzdurą (pomijam już kwestię, łagodnie mówiąc, braku precyzji sformułowania 'udowodnienie ... jest nierozstrzygalne'). Bo przecież w "On Computable Numbers, with an Application to the Entscheidungsproblem" Turing _udowodnił_, że maszyna nie umie rozwiązać pewnego typu problemu.

Aha, pojmuję Twoją logikę. Zakładasz, że Turing był komputerem, zatem fakt udowodnienia przez niego nierozstrzygalności pewnego problemu dowodzi, że takie dowody są rozstrzygalne. Mylisz się w tym punkcie, w którym twierdzisz, że Turing jest komputerem. W najlepszym wypadku popełniasz błędne koło.

Ja potrafię udowodnić, że sprawdzenie, do której klasy złożoności należy dany system formalny, jest nierozstrzygalne. Bez odwoływania się do żadnych tez, że człowiek jest albo nie jest komputerem.

Cytuj
Co to znaczy, że system formalny jest rozstrzygalny?
Co to znaczy, że udowodnienie jest nierozstrzygalne?

System formalny jest rozstrzygalny, jeżeli można napisać algorytm, który przetestuje prawdziwość każdego zdania w tym systemie.
Zadanie udowodnienia rozstrzygalności systemu: mamy dany system formalny i musimy powiedzieć "tak", jeśli jest rozstrzygalny lub "nie" w przeciwnym wypadku. Zadanie to jest nierozstrzygalne, czyli nie istnieje algorytm, który to zrobi.

Cytuj
Nie możesz mieć możliwości sprawdzenia prawdziwości _każdego_ twierdzenia. Nic nie stoi natomiast na przeszkodzie, być mógł sprawdzić _niektóre_ z nich. Chyba nie wierzysz, że nie potrafisz znaleźć np. trywialnych błędów logicznych albo arytmetycznych...

Pytam się, jak wyobrażasz sobie sytuację, że moja "rozstrzygalność" wyjdzie na jaw. Jeżeli zdaję sobie sprawę ze swojej "rozstrzygalności", to automatycznie staję się "nierozstrzygalny".
Błąd w moim rozwiązaniu być może będzie trywialny, ale nie powinienem móc go zauważyć, bo jeśli go zauważę, to go usunę.

Cytuj
ROTFL! No ale co jest w tym kontrowersyjnego? Masz aksjomaty i reguły wynikania, więc generowanie dowodów to czynność typograficzna - zastępowanie jednych symboli innymi.

ROTFL, że nie wierzę Ci na słowo?
zęsto w jednym kroku dowodu mamy nieskończenie wiele alternatywnych dróg. Np. masz udowodnić, że "istnieje liczba, która robi coś tam". Nic prostszego - wystarczy znaleźć tą liczbę. Ale ponieważ liczb jest nieskończenie wiele, komputer ma nieskończenie wiele alternatyw do rozważenia. Dlatego potrzebny jest człowiek, który przyjdzie i wpisze tą liczbę.
I domagam się, żebyś mi pokazał algorytm udowadniający twierdzenie Goedla (w zadanej teorii). Ewentualnie wskaż publikację, gdzie go znajdę.

Cytuj
to, że człowiek w przypadku interaktywnych proverów bierze udział w procesie dowodzenia, nie wynika z tego, że komputer 'sam nie będzie tego umiał', tylko ze względów praktycznych

Nie. Wynika to ze względów fundamentalnych. Komputer nigdy by tego bez człowieka nie zrobił, i to nie ze względu na brak zasobów.

Cytuj
h: 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.
N: Twierdzenie Goodsteina dla PA.

OK, dołączamy do arytmetyki twierdzenie Goodsteina jako dodatkowy aksjomat. Wskaż zdanie Goedla dla tej nowej teorii.

Cytuj
No ale my mówimy tu o problemach nierozstrzygalnych. Które, rzekomo, potrafisz rozwiązać - innymi słowy, dla każdej instancji takiego problemu potrawisz znaleźć rozwiązanie. Co jest trochę naiwne - to tak jakbyś napisał program analizujący składnię algorytmów np. pod kątem warunków pętli, przetestował go na kilkunastu przypadkach, po czym doszedł do wniosku, że Twój algorytm potrafi rozwiązać problem stopu.

Nawiązując do Twojej analogii, przeanalizowałem tyle miliardów przypadków, że uznałem, że dalej mi się nie chce, bo widocznie potrafię przeanalizować wszystkie.
Jeżeli człowiek jest maszyną Turinga, to tablica rozwiązań problemów nierozstrzygalnych zamknięta w jego głowie jest tak ogromna, że jeszcze nie doszliśmy do jej końca.

Cytuj
Ależ skąd. Czy aby rozstrzygnąć prawdziwość zdania (p)^(~p), musisz rozstrzygnąć, czy p jest prawdziwe, albo fałszywe?

A jeszcze niedawno twierdziłeś, że dowód twierdzenia Goedla jest konstruktywny.

Cytuj
Czy znając dowód Goedla, potrafisz rozstrzygnąć, że np. ZFC jest niezupełna, czy też może jest sprzeczna?

Nie potrafię, ale gdybym miał maszynkę do dowodzenia twierdzenia Goedla, to bym potrafił.

Cytuj
No ale dowód, który mój algorytm zwrócił jako wynik, nie powie Ci, czy Twoja teoria okazała się niezupełna, czy sprzeczna. Mój algorytm powie Ci tylko, że dowolna teoria zawierająca arytmetykę musi być albo sprzeczna, albo niezupełna...

OK, zdecydowałeś, że Twój dowód twierdzenia Goedla będzie niekonstruktywny. W porządku, dostosuję się. W jaki sposób Twój algorytm będzie w takim razie dowodził, że każdy system jest sprzeczny lub niezupełny? Konstruując zdanie Goedla?
Prepara tu palo en mano, que hay vienen los hombres malos.
Prepara tu palo hermano, que hay vienen los hombres malos.

Offline Neratin

Człowiek a komputer
« Odpowiedź #12 dnia: Lipiec 29, 2007, 08:06:09 pm »
Cytat: "haael"
Z komputerem jest tak samo. On też nie oblicza wszystkich instancji problemu, tylko niektóre, dopóki mu prądu nie wyłączą.

Dlatego używamy formalizmu maszyny Turinga, lub równoważnych.

Cytuj

Aha, pojmuję Twoją logikę.

Najwyraźniej nie pojmujesz.

Cytuj
Zakładasz, że Turing był komputerem, zatem fakt udowodnienia przez niego nierozstrzygalności pewnego problemu dowodzi, że takie dowody są rozstrzygalne. Mylisz się w tym punkcie, w którym twierdzisz, że Turing jest komputerem. W najlepszym wypadku popełniasz błędne koło.

No ale jeszcze raz: co to są 'dowody rozstrzygalne'?

I dlaczego uważasz, że Turing mógł wyprowadzić dowód nierozstrzygalności Entscheidungsproblem, a nie istnieje mechaniczna procedura która może zrobić to samo, skoro sama idea formalnego dowodu zakłada, że musi składać się on ze skończonej liczby operacji symbolicznych, dzięki którym potrafimy dojść od zbioru aksjomatów do twierdzenia?

Cytuj

Nie, nie mylę.
Ja potrafię udowodnić, że sprawdzenie, do której klasy złożoności należy dany system formalny, jest nierozstrzygalne. Bez odwoływania się do żadnych tez, że człowiek jest albo nie jest komputerem.

Serio?

Cytuj
System formalny jest rozstrzygalny, jeżeli można napisać algorytm, który przetestuje prawdziwość każdego zdania w tym systemie.
Zadanie udowodnienia rozstrzygalności systemu: mamy dany system formalny i musimy powiedzieć "tak", jeśli jest rozstrzygalny lub "nie" w przeciwnym wypadku. Zadanie to jest nierozstrzygalne, czyli nie istnieje algorytm, który to zrobi.

Ponownie się mylisz... dla _danego_ systemu formalnego, np. rachunku predykatów pierwszego rzędu, istnienie takiego algorytmu który zweryfikuje jego rozstrzygalność, _jest_ możliwe. Co ponownie pokazał Turing.

Cytuj
Pytam się, jak wyobrażasz sobie sytuację, że moja "rozstrzygalność" wyjdzie na jaw.

Nie wiem. To Ty twierdzisz, że zostało matematycznie udowodnione, że potrafisz rozwiązywać problemy nierozstrzygalne.

Cytuj
ROTFL, że nie wierzę Ci na słowo?
zęsto w jednym kroku dowodu mamy nieskończenie wiele alternatywnych dróg.

I co z tego? Startujemy ze skończoną, albo w najgorszym razie przeliczalną liczbą aksjomatów, oraz reguł wynikania. Wypróbowujemy je po kolei, generując kolejne twierdzenia. Każdy dowód formalny ma skończoną długość, co oznacza, że _zawsze_ go osiągniemy w skończonej ilości kroków.

Cytuj
Np. masz udowodnić, że "istnieje liczba, która robi coś tam". Nic prostszego - wystarczy znaleźć tą liczbę. Ale ponieważ liczb jest nieskończenie wiele, komputer ma nieskończenie wiele alternatyw do rozważenia. Dlatego potrzebny jest człowiek, który przyjdzie i wpisze tą liczbę.


Serio? Tak sobie wyobrażasz 'ludzkie' dowody? Że ktoś zgaduje jakąś liczbę, i voila?

To byłoby fajne, ale:
1) gdyby chodziło tylko o znalezienie takiej liczby, którą _potrafi_ wpisać człowiek, komputer i tak potrafiłby to zrobić w skończonym czasie, po prostu sprawdzając po kolei wszystkie alternatywy. Jeśli taka liczba istnieje, dojdzie do niej prędzej czy później.
2) Metoda ta nie zadziała, jeśli mamy udowodnić, że nie istnieje liczba, która robi coś tam (np. mamy udowodnić hipotezę Goldbacha). Tyle że w takim przypadku także człowiek nas nie poratuje.



Cytuj

I domagam się, żebyś mi pokazał algorytm udowadniający twierdzenie Goedla (w zadanej teorii). Ewentualnie wskaż publikację, gdzie go znajdę.

Przecież już Ci pokazałem, książkę Shankara możesz kupić np. na Amazonie. Ideę dowodu O'Connora możesz znaleźć tutaj
http://r6.ca/Goedel/TPHOLS2005_incompleteness.pdf

Cytuj

Nie. Wynika to ze względów fundamentalnych. Komputer nigdy by tego bez człowieka nie zrobił, i to nie ze względu na brak zasobów.

Dlaczego 'nigdy'? W którym miejscu dowód Goedla jest nie do wyprowadzenia przez komputer?

Cytuj
OK, dołączamy do arytmetyki twierdzenie Goodsteina jako dodatkowy aksjomat. Wskaż zdanie Goedla dla tej nowej teorii.

"To zdanie nie jest dowodliwe w nowej teorii".

Cytuj

Nawiązując do Twojej analogii, przeanalizowałem tyle miliardów przypadków, że uznałem, że dalej mi się nie chce, bo widocznie potrafię przeanalizować wszystkie.

To w dalszym ciągu nie dowodzi, że potrafisz rozwiązywać problemy nierozstrzygalne...

Cytuj
Jeżeli człowiek jest maszyną Turinga, to tablica rozwiązań problemów nierozstrzygalnych zamknięta w jego głowie jest tak ogromna, że jeszcze nie doszliśmy do jej końca.


To samo można byłoby powiedzieć o komputerach - liczba problemów rozstrzygalnych jest w końcu przeliczalna.

Cytuj

A jeszcze niedawno twierdziłeś, że dowód twierdzenia Goedla jest konstruktywny.

A nie jest? Twierdzenie Goedla mówi, że istnieje pewne zdanie, którego nie można udowodnić, jeśli system formalny jest niesprzeczny. Dowód Goedla podaje sposób konstrukcji tego zdania. Gdzie tu brak konsruktywności?

Cytuj

Nie potrafię, ale gdybym miał maszynkę do dowodzenia twierdzenia Goedla, to bym potrafił.

ROTFL! Jakim cudem?

Weźmy Twoją próbę dowodu, której centralną częścią jest to stwierdzenie:

"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."

Jak dla mnie, 'udowodniłeś' na razie, że istnieją dwa sposoby dowodzenia zdania G(S). Jednym z nich jest udowodnienie twierdzenia Goedla (z którego G(S) wynika w trywialny sposób), drugim z nich jest zademonstrowanie, że teoria S jest niezupełna, lub że jest sprzeczna.

Po czym, nie wiadomo jakim skokiem myślowym, doszedłeś do wniosku, że algorytm który dowodzi twierdzenie Goedla wykorzystuje drugą metodę, przechodząc po wszystkich zdaniach G(S). I na tej podstawie wyciągnąłeś jakieś wnioski dotyczące problemu stopu.

Cytuj

OK, zdecydowałeś, że Twój dowód twierdzenia Goedla będzie niekonstruktywny.

Nie, nie zdecydowałem... dowód twierdzenia Goedla byłby niekonstruktywny, gdyby udowodniono tylko istnienie takiego zdania, bez podania sposobu jego konstrukcji.

Cytuj
W porządku, dostosuję się. W jaki sposób Twój algorytm będzie w takim razie dowodził, że każdy system jest sprzeczny lub niezupełny? Konstruując zdanie Goedla?

Tak, w taki sam sposób, jak zrobił to Goedel. Ideę masz na końcu u O'Connora.

Offline MaDeR

Re: Człowiek a komputer
« Odpowiedź #13 dnia: Lipiec 31, 2007, 07:16:14 pm »
Odpowiem na mój puchatkowy rozumek. :)

Cytat: "haael"

Chciałbym zaproponować temat: w jakim stopniu procesy myślowe człowieka są powiązane z obliczeniami maszynowymi?

Czy sztuczna sieć neuronów, dokładnie duplikująca zachowanie się neuronów w ludzkim mózgu, to komputer czy człowiek?

Założenia powyższego pytania:
*Możliwe jest zbudowanie takiej sieci. Uważam to za pewne - codziennie miliony ludzi z zapamiętaniem próbuje tworzyć nowe sieci neuronowe, a zbudowanie sztycznych odpowiedników to kwestia wyłacznie technologii, a nie jakichś praw fizyki, które by to zabraniały czy coś w tym rodzaju.
*Taka sieć wystarczy, by wygenerować ludzki umysł.

Z drugim założeniem może być zabawa. :)

Cytat: "haael"
Czy człowiek jest komputerem?

Nie.

Cytat: "haael"
Czy uda się kiedyś zrobić komputer obdarzony świadomością?

Tak.
Sanity is overrated.
Poznaj się z Świadkiem Wszechświata

Offline Neratin

Re: Człowiek a komputer
« Odpowiedź #14 dnia: Sierpień 01, 2007, 09:54:52 am »
Jest tylko kilka ale (tzn. dodatkowych założeń)

1. Czy jest możliwe symulowanie, przy pomocy jakiegoś fizycznego urządzenia, umysłu ludzkiego?

a) nie - bo np. za świadomość odpowiada transcendentne zjawisko duszy, jak uważa Haael.
b) tak - pogląd np. Penrose'a.

W ramach punktu b) mamy do wyboru następujące ewentualności:

i) jest to fizyczna realizacja maszyny Turinga (czyli, ujmując rzecz kolokwialnie 'człowiek jest komputerem').
ii) jest to fizyczna realizacja silniejszego formalizmu (pogląd Penrose'a).

Problem z punktem ii) jest taki, że jak już zauważył Haael, nie znamy procesu fizycznego, który umożliwiłby konstrukcję maszyny silniejszej obliczeniowo od maszyny Turinga (a dokładniej, probabilistycznej MT).
Penrose twierdzi, że taka maszyna jest do zbudowania w ramach nowej, nieodkrytej jeszcze fizyki, byłoby jednak bardzo dziwne, gdyby fenomenologia kwantowej teorii grawitacji pozostawała poza zasięgiem naszych urządzeń pomiarowych i jednocześnie jakieś jej, nie takie subtelne efekty były wykorzystywane przez makroskopowe, fizyczne urządzenie jakim jest ludzki mózg.

BTW, sieci neuronowe, jakie się dzisiaj buduje, są pod względem mocy obliczeniowej równoważne maszynie Turinga, więc symulacja ludzkiego mózgu przy ich pomocy dowiodłoby, że człowiek _jest_ komputerem.