GIM, nastavak

(za uklapanje u kontekst, prethodno bi bilo dobro
pro~citati Pad Hilbertovog programa)


[lesson no=8 part=2]
Dakle, sto je pisalo u munji koja je
razorila Hilbertov program?

[spoiler/ type="Waitapu/*citala:-?*/"
comment="ovo ce vjerojatno utjecati na tvoje poimanje istine,
dokazivanja i ostalih stvari koje je math iscupala iz njihovog
prvobitnog stanista kako bi od njih ucinila
nesto puno preciznije i zabavnije - jesi li spremna na to:-?...
Ma znam da jesi, samo te zezam...:-)"]

Pisalo je nesto ovakvo:
	G:=!ID(!ID) .
Da, znam, u pocetku se covjek osjeca pomalo poput onih filozofa
koje je Duboka Misao
(citala Vodic kroz galaksiju za autostopere:-?)
"razveselila" brojem 42 [:-/] :-)... no pogledajmo detaljnije:

pretpostavimo da G nije istinita. (Zapamti ovu pretpostavku.:)
Tada: G nije istinita => !ID(!ID) nije istinita =>
=> ID(!ID) jest istinita => dvostruki !ID je ispisiv =>
=> !ID(!ID) je ispisiv(a) => !ID(!ID) je istinita =>
=> G je istinita. Ups.
[style name="Al Bundy"]
Now, _that_'s what I call a contradiction!
[/style] :-/

Ok, dakle pretpostavka "G nije istinita" vodi na kontradikciju.
Dakle, G jest istinita.
(Onda zaboravi pretpostavku i zapamti ovaj zakljucak.:)
No tada:
G je istinita => !ID(!ID) je istinita =>
=> ID(!ID) nije istinita =>
=> dvostruki !ID nije ispisiv => !ID(!ID) nije ispisiv(a) =>
=> G nije ispisiva.
Dakle, G nije ispisiva.

Sto imamo? Imamo recenicu G ,
koja rusi sve nade u ispunjivost projekta GIM2 ...
istinita je, ali beznadno neispisiva od strane
GIMolikih sistema, jer upravo njena istinitost
lezi u njenoj neispisivosti...

A sad, kakve to veze ima s Goedelovim radom:-? Kao sto rekoh
na pocetku, to je ideja... Goedel je imao puno vise posla
primjenjujuci je na (+PA+) nego sto smo mi imali
primjenjujuci je na "GIM|-"-svijet...
no kad covjek jednom kuzi ideju, tehniku je puno lakse provesti
(iako, naravno, necu ici u sve detalje u mailu:)...


((ovdje ulazi tekst Aksiomatizacija
matematike ~ za~sto je utopija?))

Skica dokaza pravog Goedelovog teorema se
iz dokaza nemogucnosti postojanja GIMa2 dobiva
prilicno jednostavno: samo find&replace
"ispisivo"->"dokazivo",
GIMovo pravilo korektnosti -> logicka pravila
zakljucivanja, neke "moralno pozitivne"
ispisive recenice -> aksiomi (+PA+)...
jasno ovo (otprilike):-?
Namjesto ! I D ( ) sada imamo nesto poput
0 ' + * = <= v ` A -> ! ( ) ...
izrazi su nesto tipa "v<=`A->!'+",
dok su recenice nesto tipa "Av`(v`+0=v`)" ili
"Av`Av``(v`*v``=v``*v`)",
ili pak "Av`Av``!(v`+0'<=v``*0'')"...
(prvo je aksiom, drugo istinita recenica koja nije aksiom,
ali se moze dokazati ("ispisiva" je, u GIM-terminologiji:),
a trece neistinita recenica...
"'" znaci "sljedbenik",
tako da je npr 0'' oznaka za broj 2 ...)
ako ti se da, sad mozes pokusati izraziti
npr. Fermatov teorem, Goldbachovu hipotezu
ili cinjenicu da je broj 6 savrsen:-) gornjim
jezikom, ali mislim da to i nije bas tako zanimljivo, a
_jako_ je dugacko... bez nekih zgodnih pokrata...
o kojima cemo jednom drugom prilikom...

E sad, netko se moze pitati:
dobro, ovaj GIM jest jako jednostavan, ali ima zgodnu osobinu
da govori o sebi: o svojem ispisivanju,
o @izrazima koji su upravo objekti njegovog govora itd. ...
(+PA+) ne govori _o_ dokazivanju aritmetickih tvrdnji,
ona govori o prirodnim brojevima... ili mozda ipak... :-? :-)
Glavna stvar koju je ovdje Goedel napravio je
da je shvatio da je recenica "(+PA+) govori o...[necemu]"
_vrlo_ subjektivna stvar
(to vidimo samo mi izvana, (+PA+) to ne vidi)...
odnosno da je moguce napraviti jedan
fantasticno mocan find&replace
koji pokazuje da (+PA+) _moze_ govoriti o samoj sebi...
kod GIM-jezika je to vrlo jednostavno...
ako si pazljivo citala,
primijetila si da nigdje nisam spomenuo
ekvivalent D-a u (+PA+) ...
u GIM-jeziku D je upravo ono sto omogucuje da se
"izjava" (npr. "I") shvati kao agrument same sebe
(npr. "I(I)" )...
no treba imati na umu da je GIM-semantika upravo konstruirana
kako bi se lako istaknuo taj point...
(+PA+) je ipak radena s cisto drugom svrhom:-), tako da je
Goedelu trebalo par godina da sve poslozi na prava mjesta...
no krajnji rezultat djeluje zacudujuce i dovoljno zanimljivo
da daje osjecaj da se takvo sto definitivno isplatilo...

Jednostavno, Goedel je (otprilike) gornjim simbolima,
izrazima, recenicama, pa cak i dokazima,
pridruzio prirodne brojeve na jedan vrlo uniforman nacin,
te izrazio razna logicka zakljucivanja kao odgovarajuce
operacije na tim brojevima, koje je (ie, operacije)
definirao samo pomocu +, *, = i <= , dakle koristeci se
u krajnjoj liniji samo sredstvima (+PA+) ...

Goedel u svom maestralnom djelu
(ne, necu navoditi njemacki naslov;)
"O formalno neodlucivim tvrdnjama
'Principie Mathematice' i ostalih srodnih sustava"
krece od nekih definicija i teoremcica u (+PA+) ,
koji se gomilaju u pocetku naizgled bez svrhe i reda,
da bi nakon 20ak gusto ispisanih stranica
kulminirali necim sto covjeka lupi osjecajem
slicnim onom kad skuzi da "!ID(!ID)" upravo
kaze "Ja nisam ispisiva>:->.",
samo puno veceg intenziteta, jer ovdje se ne radi
o teorijici koja se da objasniti (pa makar samo ofci;)
na 3 ekrana ASCII-teksta,
vec se radi o necemu cemu smo bili voljni
predati svu matematiku u ruke:-/...

Da bi malo bolje skuzila o cemu se tu radi,
i kako GIM moze pricati o sebi cak i kroz prirodne brojeve
(ako treba:), promotri (hm, kako da ga nazovem...:)
BGIMa (Binary GIM, ili Better GIM:),
koji je u mnogocemu slican GIMu, osim sto
(na prvi pogled) nije tako egocentrican...
on kao fol prica o prirodnim brojevima... :-)

Dakle, BGIM:
(Navodit cu uglavnom samo detalje koji se razlikuju,
ako zelis, napisi kompletnu pricu...:)
Abeceda mu je ! I # 0 1 .
Prirodne brojeve ovdje gledamo kao
njihove binarne zapise, cisto radi jednostavnosti...

Sad uvodimo jedan novi pojam,
koji obicnom GIMu nije trebao... kod (s dugim 'o':).
Kod pojedinih slova je dan sljedecom tablicom
	'!'	10
	'I'	100
	'#'	1000
	'0'	10000
	'1'	100000
("Slova" su znakovi, njihovi kodovi su binarni brojevi...)
Kod nekog izraza dobije se jednostavnim "nastukavanjem"
kodova pojedinih slova, npr. kod od "0#!" je 10000100010 ...
kod praznog izraza ("") mozemo staviti npr. da je 0
zbog potpunosti, iako sumnjam da ce ti zatrebati...:-)

Ulogu dvostrukih izraza sad preuzimaju "cupavi" izrazi...
(prvo slovo u rijeci "cupavi" je 4. slovo hrvatske abecede:)
((taj cudan naziv je posvecen Nuni, asistentu iz RP1, koji
'#'-znakove zove "cupavcima":-)... tko zna zasto sam se bas
sad toga sjetio...:))
"cupavi" izraz X je X iza kojega je nastukan njegov kod
shvacen kao niz slova '0' i '1' ... npr. cupavi "0#!" je
"0#!10000100010" ...
cupavi "1" je "1100000" - primijeti da ovo nije
broj, vec izraz... cupavi "" je "0" ,
kad smo vec kod toga...:-)
Dakako, intuitivna interpretacija od '!' i 'I' je ista kao u
GIMa, dok je intuitivna interpretacija
'#'a pridjev "cupavi"...

Neka je Y genericka oznaka za kod nekog izraza, shvacen kao
izraz, npr. Y0:="100010" ... lako se vidi da svaki Y
moze biti kod samo jednog izraza, pa taj izraz oznacimo
s E(Y) ... npr. E(Y0)="#!" , E("0")="" , dok npr. E("110") i
E("1!") nisu definirani... (smijem pitat jel jasno:-? :)

Dakle, recenice su izrazi jednog od sljedecih tipova:
IY ; istinita :akko je E(Y) ispisiv...
I#Y ; istinita :akko je cupavi E(Y) ispisiv...
!IY ; istinita :akko IY nije istinita... ili
!I#Y ; istinita :akko I#Y nije istinita...
(npr. "I100010" jest recenica, dok "I110" _nije_, jer
110 nije kod nijednog izraza, pa "110" nije valid Y ...)
[note type="funny"]kod drugog tipa je vise-manje
svejedno zamijenimo li "cupavi" i "E" , jer je
cupavi E(Y) = E(cupavi Y) ,
ako su oba ta izraza definirana (Y!="" & Y!="0"), npr.
cupavi E(Y0) = cupavi "#!" = "#!100010" ;
E(cupavi Y0) = E(cupavi "100010") =
= E("10001010000010000100001000010000010") = "#!100010"
/probaj ovo dokazati ako ti se da...:-)/; ali to
nije bitno za nastavak...[/note]

Sad mozemo vidjeti da su ova dva GIMa zapravo skoro pa
izomorfna (sto moze jedan, moze i drugi..., odnosno,
postoji jednostavan find&replace koji "Psihologiju GIMa"
prevodi u "Psihologiju BGIMa", i natrag...:), samo sto
su BGIMu izrazi "o kojima prica" binarni brojevi, a ne
vise njegovo vlastito ponasanje. No, lako je vidjeti da
i BGIM ima Goedelovu recenicu,
	G_B:="!I#101001000" .

Dakako, (ovo mozes i sama raspisati, ja samo pisem da vidim
nisam li nesto zabrljao u definicijama /nisam se bas
_pripremio_ za ovo "predavanje":/...:)
G_B istinita <=> "!I#101001000" istinita <=>
<=> "I#101001000" neistinita <=>
<=> cupavi E("101001000") nije ispisiv <=>
<=> cupavi "!I#" nije ispisiv <=>
<=> "!I#101001000" nije ispisiv(a) <=>
<=> G_B nije ispisiva ,
pa pretpostavka o neistinitosti od G vodi na kontradikciju
s korektnoscu, dakle G je istinita i samim time neispisiva.

Naravno, ovo (prijelaz GIM->BGIM , i G->G_B) je
bilo jednostavno, no dobro ilustrira ideju da
"ono o cemu govorimo" _ne_ pise u izrazu, vec u semantici
(nasoj interpretaciji tog izraza)...
((to je ono gore gdje pise kada su
koji tipovi recenica istiniti))
Jel sad jasnije da npr. "Av`Av``(v`*v``=v``*v`)"
(kao recenica u (+PA+) ) _ne_ mora pricati o
komutativnosti mnozenja (ako si to uopce pomislila
in the first place:), vec moze pricati o bilo cemu sto ima
dovoljno slicnu logicku strukturu [:-?].
Goedel je pokazao da dokazivanje u (+PA+)
(kao i u svim ostalim formalnim sistemima dovoljno dobrim
da bismo ih htjeli za vrhovne vladare matha) _ima_ dovoljno
slicnu logicku strukturu strukturi prirodnih brojeva,
i time dobio G za (+PA+) , pokazavsi da je
Hilbertov program (koji se bazirao na Russelu & Whiteheadu,
izmedu ostalih) utopija koja nikad nece biti postignuta...

Ovoga stvarno ima _puno_... The End (zasad:)
[/lesson]