Tko ce smisliti veci broj

[The Avenger]

Evo ga: "Najveći broj!"

[Bredon]

skeptik kaže:

Bitno je još naglasiti da se radi o ZFC prvog reda, dakle ZFC u kojem se koristi samo logika prvog reda, odnosno logika u kojoj nije dozvoljeno kvantificiranje nad skupovima. Jako je dobro poznato da je logika prvog reda vrlo ograničavajuća, tj. da se s njom mnoge stvari ne mogu dokazati. Primjerice Goodstein-ov teorem se ne može dokazati s Peanovim aksiomima prvog reda, ali može s Peanovim aksiomima drugog reda.

Intuitivno gledano, kvantificiranje nad skupovima, dakle logika drugog reda, je nešto vrlo prirodno što koristimo čak i u svakodnevnom jeziku, tako da je s te strane dosta neprirodno ograničavati se na logiku prvog reda. No logičari se ipak vole tako ograničavati, jer logika prvog reda ima neka lijepa svojstva koja logika drugog reda nema.

To što si napisao nije baš točno. U ZFCu prvog reda možeš kvantificirati preko skupova; dapače, radiš to svaki put kad kvantifciraš u ZFCu (ako shvaćaš elemente svog modela ZFCa kao skupove). Zapravo se sva matematika, osim možda nekih specijaliziranih teorijsko-skupovnih stvari, radi u ZFCu prvog reda, odnosno ZFC drugog reda nije nešto intuitivniji od ZFCa prvog reda.

Teorija ZFCa drugog reda je nešto malo suptilnija, a ni meni nije bilo skroz jasno što bi bila dok nisam guglao, ali vrijedi spomenuti da se i poznati logičari to pitaju (zanimljivo je primijetiti da je pitanje postavio Harvey Friedman).

[Leteća]

Jel već bilo pun kurac i osamsto?

[Bredon]

I još nešto sam se sjetio:

skeptik kaže:

Zanimljivo. Išao sam si malo pročitat o tome, bacio sam pogled i na njihov originalni rad, pa sam onda to sebi intuitivno objasnio ovako. Turing je još davno dokazao da je halting problem neodlučiv. No iako je Turingov dokaz relativno jednostavan i kratak, dokaz ne slijedi iz ZFC aksioma. Potrebno nam je nešto izvan ZFC aksioma da bismo dokazali Turingov teorem o neodlučivosti halting problema.

Imaš li neku referencu za to da Turingov dokaz ne prolazi u ZFCu? Ne znam sad dokaz napamet, ali ne vidim što to točno ne bi prošlo. A i mislim da bih znao da ne prolazi...

Jedini rizik s dokazom eksplicitno u ZFCu bi bio da postoji program koji rješava halting problem, a koji nije izraziv u ZFCu - ali to je onda rizik svugdje.

[vamvam]

Vezano uz halting problem, što točno znači "da je neodlučiv" ili "da se ne može riješiti"?

[skeptik]

vamvam kaže:

Vezano uz halting problem, što točno znači "da je neodlučiv" ili "da se ne može riješiti"?

Znači da ne postoji algoritam (kompjuterski program) koji bi odgovorio na to pitanje.

[Bredon]

vamvam kaže:

Vezano uz halting problem, što točno znači "da je neodlučiv" ili "da se ne može riješiti"?

skeptik kaže:

Znači da ne postoji algoritam (kompjuterski program) koji bi odgovorio na to pitanje.

Da, tako nešto. S tim da se halting problem nikad ne dokazuje za same algoritme, jer ne postoji formalna definicija algoritma, već se dokaže za određene modele komputacije.
(Recimo, na razini samih algoritama bismo mogli iskazati nerješivost halting problema tako da kažemo da ne postoji algoritam takav da, uzimajući kao input bilo koji algoritam i njegov input, u konačno vrijeme kaže hoće li taj algoritam s tim inputom završiti u konačno mnogo koraka ili će se vječno vrtjeti.)

Zato uzimamo Turingove strojeve i vjerujemo u Church-Turingovu tezu, te onda dokazujemo nerješivost halting problema za Turingove strojeve, odnosno da ne postoji Turingov stroj takav da "zna" dovršavaju li drugi Turingovi strojevi svoj rad ili ne.

[wand_1]

Bredon kaže:

Da, tako nešto. S tim da se halting problem nikad ne dokazuje za same algoritme, jer ne postoji formalna definicija algoritma, već se dokaže za određene modele komputacije.
(Recimo, na razini samih algoritama bismo mogli iskazati nerješivost halting problema tako da kažemo da ne postoji algoritam takav da, uzimajući kao input bilo koji algoritam i njegov input, u konačno vrijeme kaže hoće li taj algoritam s tim inputom završiti u konačno mnogo koraka ili će se vječno vrtjeti.)

Zato uzimamo Turingove strojeve i vjerujemo u Church-Turingovu tezu, te onda dokazujemo nerješivost halting problema za Turingove strojeve, odnosno da ne postoji Turingov stroj takav da "zna" dovršavaju li drugi Turingovi strojevi svoj rad ili ne.

Sad imam koga pitati za modele hiperkomputacije, odnosno komputacije van granica Church-Turingove teze.

Kako je ta stvar u prinicpu 'nemoguća', rijetko se može sresti, a relativno davno sam čitao knjigu o Super Turingovoj komputaciji. U teoriji je često sresti poneki Turing oracle, ali koliko znam, nitko ne govori o modelima hiperkompjutera.

Moje (teorijsko) pitanje za tebe je da li (možebitne) zatvorene vremenolike podržavaju hiperkomputaciju?

Konkretno, sjećam se da bi se kompjuter koji radi u Malament-Hogardtovom prostor-vremenu može na određen način funkcionirati kao relativistički hiperkompjuter. Takav kompjuter, navodno, mogao bi u polinomijalnom vremenu rješavati P-SPACE kompletne probleme?

Ili ako hoćeš drugačije - zašto to nije moguće?

[vamvam]

skeptik kaže:

Znači da ne postoji algoritam (kompjuterski program) koji bi odgovorio na to pitanje.

A kako je Turing to izračunao ako ne postoji algoritam koji to računa?

[skeptik]

vamvam kaže:

A kako je Turing to izračunao ako ne postoji algoritam koji to računa?

Turing je ljudsko biće, a ne kompjuter. Ljudski način rezoniranja nije uvijek algoritamski. Algoritam, da bi radio, mora imati zadana pravila po kojima radi. Ta pravila mu zadaje programer, dakle ljudsko biće. Čovjek, kada smišlja ta pravila, to ne čini algoritamski. U svrhu smišljanja pravila čovjek koristi svoju intuiciju. Za razliku od ljudi, kompjuteri nemaju intuiciju. Zato ljudi mogu dokazati teoreme koje kompjuteri ne mogu. Najslavniji primjer, usko povezan sa Turingovim teoremom, je Godelov dokaz da u aritmetici postoje istinite tvrdnje koje se ne mogu dokazati nikakvim algoritmom. Poanta je da je to dokazao Godel, a ne kompjuter. Kompjuter ne može dokazati Godelov teorem. Čovjek može.

[vamvam]

skeptik kaže:

Turing je ljudsko biće, a ne kompjuter. Ljudski način rezoniranja nije uvijek algoritamski. Algoritam, da bi radio, mora imati zadana pravila po kojima radi. Ta pravila mu zadaje programer, dakle ljudsko biće. Čovjek, kada smišlja ta pravila, to ne čini algoritamski. U svrhu smišljanja pravila čovjek koristi svoju intuiciju. Za razliku od ljudi, kompjuteri nemaju intuiciju. Zato ljudi mogu dokazati teoreme koje kompjuteri ne mogu. Najslavniji primjer, usko povezan sa Turingovim teoremom, je Godelov dokaz da u aritmetici postoje istinite tvrdnje koje se ne mogu dokazati nikakvim algoritmom. Poanta je da je to dokazao Godel, a ne kompjuter. Kompjuter ne može dokazati Godelov teorem. Čovjek može.

Pa zar nije poanta dokazivanja u tome da formalno dokažeš (ili osporiš) ono što ti je intuitivno (ne)jasno? Svakome je intuitivno jasno da ne postoji broj koji je i paran i neparan, ali dokaz toga dokaz, a intuicija je intuicija.

[wand_1]

vamvam kaže:

Pa zar nije poanta dokazivanja u tome da formalno dokažeš (ili osporiš) ono što ti je intuitivno (ne)jasno? Svakome je intuitivno jasno da ne postoji broj koji je i paran i neparan, ali dokaz toga dokaz, a intuicija je intuicija.

Pogledaj malo neki popularniji prikaz Godelovog dokaza, ovo ti je vrlo slično tome, zapravo isti se i koristi u Turingovom dokazu.

[skeptik]

vamvam kaže:

Pa zar nije poanta dokazivanja u tome da formalno dokažeš (ili osporiš) ono što ti je intuitivno (ne)jasno? Svakome je intuitivno jasno da ne postoji broj koji je i paran i neparan, ali dokaz toga dokaz, a intuicija je intuicija.

Svaki formalni dokaz uzima zdravo za gotovo neke aksiome, tj. pretpostavke koje ne možeš dokazati. Intuicija služi da dođeš do tih aksioma. Godelov teorem kaže da uvijek (za dovoljno općenit konzistentan sistem aksioma) postoji tvrdnja za koju je intuitivno očito da je istinita, ali se ne može dokazati iz tih aksioma. Jedna takva tvrdnja (tzv. Godelova rečenica), kad se prevede na obični jezik, glasi:
"Ova tvrdnja se ne može dokazati pomoću zadanog skupa aksioma."
Netrivijalna tvrdnja koju je Godel dokazao je da se takva rečenica uvijek može izreći u dovoljno općenitom sustavu aksioma.

[skeptik]

Nakon ovoga
https://www.scottaaronson.com/writings/bignumbers.html
teško da se može nešto nadodati.

[wand_1]

skeptik kaže:

Nakon ovoga
https://www.scottaaronson.com/writings/bignumbers.html
teško da se može nešto nadodati.

Da, poznato mi je to, zato sam pitao za onaj dokaz oko Busy Beavera

[Unknown Archont]

https://www.sciencedaily.com/release...0104164507.htm

[wand_1]

Unknown Archont kaže:

https://www.sciencedaily.com/release...0104164507.htm

Svako par tjedana novi najveći prim broj..