Шумадијски блуз

Na pr­vom me­stu, ne­ko­li­ko op­štih na­po­me­na o na­šem pred­me­tu. Iz­ra­ze „mo­der­na lo­gi­ka“ i „ma­te­ma­tič­ka lo­gi­ka“ raz­u­me­mo kao si­no­nim­ne. Da­kle, pod mo­der­nom lo­gi­kom pod­ra­zu­me­va­mo onu gra­nu ma­te­ma­ti­ke za­če­tu, pre sve­ga, u Fre­ge­o­vim (Got­tlob Fre­ge) ra­do­vi­ma s kra­ja XIX ve­ka, ko­ja je svo­ju ka­no­ni­za­ci­ju do­ži­ve­la u pr­vim de­ce­ni­ja­ma XX ve­ka, za­hva­lju­ju­ći, na pr­vom me­stu, ra­do­vi­ma Hil­ber­ta (Da­vid Hil­bert) i Ber­naj­sa (Paul Bernays). Raz­u­me se, mo­der­na lo­gi­ka ima ja­ko du­gu pred­i­sto­ri­ju ko­jom do­mi­ni­ra Ari­sto­te­lo­va si­lo­gi­stič­ka lo­gi­ka, i ko­ja lo­gi­ku si­tu­i­ra u kor­pus fi­lo­zof­skih pre ne­go ma­te­ma­tič­kih di­sci­pli­na. Po Kvaj­no­vim (Wil­lard Van Or­man Qu­i­ne) re­či­ma „lo­gi­ka je predmet sa du­gom isto­ri­jom, ko­ji je 1879. po­stao ve­li­ki“(2). Go­di­na ko­ju Kvajn na­vo­di je­ste go­di­na u ko­joj je ob­ja­vljen Fre­ge­ov Begriffsschrift, de­lo za ko­je s pra­vom mo­že­mo re­ći da pred­sta­vlja vo­do­del­ni­cu iz­me­đu „sta­re“ i no­ve, mo­der­ne lo­gi­ke.(3)

Pe­riod iz­me­đu dva svet­ska ra­ta do­veo je do ra­slo­ja­va­nja unutar lo­gi­ke, ko­je je za po­sle­di­cu ima­lo iz­dva­ja­nje če­ti­ri osnov­ne gra­ne ovog pred­me­ta. Reč je o teoriji skupova, teoriji modela, teoriji dokaza i teoriji izračunljivosti. Te­o­ri­ja sku­po­va, naj­sta­ri­ja od če­ti­ri gra­ne lo­gi­ke, na­sta­je sedam­de­se­tih go­di­na XIX ve­ka u ra­do­vi­ma ne­mač­kog ma­te­mati­ča­ra Ge­or­ga Kan­to­ra (Ge­org Can­tor). Ne­ki auto­ri ra­đa­nje ove di­sci­pli­ne ve­zu­ju za ve­o­ma kon­kre­tan da­tum, na­i­me 7. de­cembar 1873. go­di­ne, ka­da je Kan­tor pi­smom oba­ve­stio Ri­har­da De­de­kin­da (Ric­hard De­de­kind) o svom ot­kri­ću ne­pre­bro­ji­vo­sti sku­pa re­al­nih bro­je­va R.(4)  

Ra­đa­nje ne­što mla­đe, te­o­ri­je mo­de­la, obič­no se ve­zu­je za 1915. go­di­nu i rad „Über Möglichkeiten im Re­la­tiv­kalkül“(5) ne­mač­kog ma­te­ma­ti­ča­ra Le­o­pol­da Le­ven­haj­ma (Le­o­pold Löwenhe­im). U ovom ra­du, Le­ven­hajm je do­ka­zao naj­ra­ni­ju ver­zi­ju ta­ko­zva­ne Levenhajm-Skolemove teoreme, ko­ja po mi­šlje­nju mno­gih pred­sta­vlja oko­sni­cu te­o­ri­je mo­de­la. Le­ven­haj­mo­ve re­zul­ta­te je dva­de­se­tih go­di­na uop­štio nor­ve­ški ma­te­ma­ti­čar To­ralf Sko­lem (Tho­ralf Sko­lem), pa otud ime po­me­nu­te te­ore­me. Po­red ovog, iz­u­zet­no va­žnog tvr­đe­nja, Le­ven­hajm je u istom ra­du do­ka­zao da se pro­blem od­lu­či­vo­sti ra­ču­na pre­di­ka­ta sa pre­di­ka­ti­ma du­ži­ne ≥ 2 svo­di na pro­blem od­lu­či­vo­sti ra­čuna ko­ji sa­dr­ži sa­mo bi­nar­ne pre­di­ka­te, kao i da je mo­na­dič­ki ra­čun pre­di­ka­ta od­lu­čiv.(6)

Te­o­ri­ja do­ka­za ima svoj iz­vor u dru­gom od 23 pro­ble­ma koje je Hil­bert iz­lo­žio na svet­skom kon­gre­su ma­te­ma­ti­ča­ra 1900. go­di­ne u Pa­ri­zu. Hil­ber­to­va ide­ja bi­la je da, na pre­la­zu ve­ko­va, is­tak­ne ne­ka od va­žnih, otvo­re­nih pi­ta­nja, ko­ja de­vet­na­e­sto­vekov­na ma­te­ma­ti­ka osta­vlja ma­te­ma­ti­ci na­red­nog ve­ka na re­ša­vanje. Po­me­nu­ti, dru­gi Hil­ber­tov pro­blem, ti­če se kon­zi­stent­no­sti for­mal­ne arit­me­ti­ke. (7) Tre­ba­lo je do­ka­za­ti da je for­mal­na arit­meti­ka kon­zi­stent­na te­o­ri­ja, i to sred­stvi­ma ko­ja su stro­go sla­bija od sred­sta­va ko­je nu­di sa­ma for­mal­na arit­me­ti­ka. Reč je o ta­ko­zva­nim finitističkim sred­stvi­ma.(8) Na­de da je ovo mo­gu­će uči­ni­ti ko­nač­no su raz­ve­ja­ne Ge­de­lo­vim (Kurt Gödel) teoremama o nepotpunosti 1931. go­di­ne.(9) Ta­ko Gedelova druga teorema o nepotpunosti ka­že da sva­ki for­malni si­stem ko­ji sa­dr­ži for­mal­nu arit­me­ti­ku (pa ti­me i sam si­stem for­mal­ne arit­me­ti­ke), uko­li­ko je kon­zi­sten­tan, ne mo­že do­kazati sop­stve­nu kon­zi­stent­nost. Tim pre je ovo ne­mo­gu­će uči­ni­ti unu­tar ne­kog strikt­no sla­bi­jeg, fi­ni­ti­stič­kog si­ste­ma.(10)

Kon­zi­stent­nost for­mal­ne arit­me­ti­ke pr­vi je do­ka­zao ne­mač­ki lo­gi­čar Ger­hard Gen­cen (Ger­hard Gent­zen), Ber­naj­sov đak i Hil­ber­tov asi­stent u Ge­tin­ge­nu od 1935. do 1939. godi­ne. Gen­ce­nov do­kaz iz 1936. go­di­ne,(11) kao i nje­gov kasni­ji rad iz 1939.(12) (ob­ja­vljen 1943. go­di­ne) ja­sno izo­lu­ju mi­ni­mal­na sred­stva ko­ja su nam neo­p­hod­na uko­li­ko že­limo do­ka­za­ti kon­zi­stent­nost ovog for­mal­nog si­ste­ma. Ovi rezul­ta­ti ozna­ča­va­ju ro­đe­nje ordinalne analize, gra­ne te­o­rije do­ka­za ko­ja pro­u­ča­va sred­stva neo­p­hod­na za do­ka­zi­va­nje kon­zi­stent­no­sti raz­li­či­tih for­mal­nih si­ste­ma.

Ovi re­zul­ta­ti u su­štin­skom smi­slu po­či­va­ju na re­zul­ta­ti­ma nje­gove dok­tor­ske di­ser­ta­ci­je, od­bra­nje­ne 1933. go­di­ne.(13) Gen­ce­no­va te­za (14) obi­lu­je ori­gi­nal­nim ide­ja­ma, i sa­dr­ži mno­go vi­še od kli­ce ono­ga što će po­sta­ti opšta teorija dokaza, gra­na te­o­ri­je do­ka­za o ko­joj će vi­še re­či bi­ti u na­stav­ku. Teorema o eliminaciji sečenja, ko­ju je Gen­cen for­mu­li­sao i do­ka­zao (15), je­dan je od naj­lep­ših re­zul­ta­ta lo­gi­ke i ma­te­ma­ti­ke uop­šte. Ide­ja ko­joj je u svo­joj te­zi pri­stu­pio, u kon­tek­stu ko­je je po­me­nu­ta te­o­re­ma i do­ka­za­na, bila je da se, ve­o­ma ozbilj­no i sa­ve­sno, po­sve­ti pro­ble­mu ana­li­ze lo­gič­ke de­duk­ci­je. Mi­nu­ci­o­znost ko­ju je po­ka­zao u ba­vlje­nju ovim pro­ble­mom, te­ško da je do da­nas pre­va­zi­đe­na. U ove svrhe, Gen­cen je raz­vio dva si­ste­ma ana­li­ze for­mal­nih de­duk­ci­ja, sistem prirodne dedukcije i sistem sekvenata. Oba ova si­ste­ma, kao i re­zul­ta­ti nji­ho­ve ana­li­ze, za­u­zi­ma­ju va­žno me­sto ka­ko u te­o­ri­ji do­ka­za ta­ko i u mo­der­noj lo­gi­ci uop­šte.

Te­o­ri­ja iz­ra­čun­lji­vo­sti na­sta­je tri­de­se­tih go­di­na pro­šlog ve­ka, u po­ku­ša­ju da se od­go­vo­ri na na­iz­gled jed­no­stav­no pi­ta­nje - šta je to iz­ra­čun­lji­va (arit­me­tič­ka) funk­ci­ja. Kao od­go­vor na ovo pi­ta­nje, a u krat­kom vre­men­skom ra­spo­nu od sve­ga ne­ko­liko go­di­na, po­nu­đe­ni su raz­li­či­ti mo­de­li iz­ra­čun­lji­vo­sti: Tjuringove mašine,(16) re­kur­ziv­ne funk­ci­je,(17) ra­čun lamb­da,(18) kao i Po­sto­ve ma­ši­ne.(19) Svi ovi mo­de­li pred­sta­vlja­ju po­ku­šaj ma­te­ma­tič­ke for­ma­li­za­ci­je i ana­li­ze poj­ma efek­tiv­ne pro­ce­du­re ili al­go­rit­ma. Za­di­vlju­ju­ća je či­nje­ni­ca, ko­ja će ne­du­go za­tim bi­ti do­ka­za­na, da su svi ovi mo­de­li me­đu­sob­no ekvi­va­lent­ni, tj. da de­fi­ni­šu istu kla­su aritme­tič­kih funk­ci­ja. Da li ovi mo­de­li pru­ža­ju ade­kvat­nu ana­li­zu poj­ma in­tu­i­tiv­ne iz­ra­čun­lji­vo­sti? Dru­gim re­či­ma, da li je svaka in­tu­i­tiv­no iz­ra­čun­lji­va funk­ci­ja ujed­no i iz­ra­čun­lji­va pu­tem Tjuringo­ve ma­ši­ne, pri­me­ra ra­di? Da je ovo slu­čaj, tvr­di ta­kozva­na Čerč-Tjuringova teza. Iako se ne mo­že­mo na­da­ti nje­nom stro­gom do­ka­zu, bu­du­ći da do­vo­di u ve­zu je­dan in­tu­i­tiv­ni (efektiv­na iz­ra­čun­lji­vost) i je­dan for­mal­ni po­jam (Tju­ring iz­ra­čun­ljivost), u pri­log ovoj te­zi go­vo­ri či­nje­ni­ca da se sva­ka funk­ci­ja ko­ju mo­že­mo sma­tra­ti in­tu­i­tiv­no iz­ra­čun­lji­vom do sa­da po­ka­za­la kao Tju­ring iz­ra­čun­lji­va.(20)

Ova tra­di­ci­o­nal­na po­de­la, raz­u­me se, ne po­kri­va či­ta­vu da­na­ šnju lo­gi­ku. Na ovom me­stu bi­smo že­le­li da is­tak­ne­mo uti­caj te­o­ri­je ka­te­go­ri­ja, jed­ne mla­de gra­ne al­ge­bre na mo­der­nu lo­giku, i obrat­no. Sim­bi­ot­ska pri­ro­da ovog od­no­sa se mo­žda naj­lep­še vi­di u od­no­su te­o­ri­je ka­te­go­ri­ja i te­o­ri­je do­ka­za, o če­mu će još bi­ti re­či.

 

Tekst je sastavni deo rada Algoritmi, kategorije i dokazi – teme iz srpske moderne logike, objavljenog u časopisu Kultura polisa (2012)

 Reference:

(2) Qu­i­ne W. V. O., The Methods of Logic, Holt, Ri­ne­hart and Win­ston, New York 1966, str. 7.

(3) Fre­ge G., Begriffsschrift: eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Lo­u­is Ne­bert Ver­lag, Hal­le 1879. Is­tak­ni­mo na ovom me­stu da je tre­ba­lo da pro­đe vi­še od se­dam de­ce­ni­ja pre ne­go što je zna­čaj Fre­ge­o­vog po­du­hva­ta is­prav­no shva­ćen. Za ne­što dru­ga­či­je gle­di­šte, ko­je Fre­geu od­ri­če iz­ve­stan deo za­slu­ga za stva­ra­nje mo­der­ne lo­gi­ke ko­je mu se obič­no pri­pi­su­ju, do­de­lju­ju­ći ih pri­tom Bu­lu (Ge­or­ge Bo­o­le) i Per­su (Char­les Sa­un­ders Pe­ir­ce), za­in­te­re­so­va­nog či­ta­o­ca upu­ću­je­mo na: Put­nam H., Pe­ir­ce the Lo­gi­cian, Historia Mathematica, Vol. 9, 1982.

(4) Za ve­o­ma za­ni­mlji­vu i de­ta­lji­ma bo­ga­tu stu­di­ju isto­ri­je te­o­ri­je sku­po­va u pe­ri­o­du 1850-1940, za­in­te­re­so­va­nog či­ta­o­ca upu­ću­je­mo na: Fer­re­i­ros J., Labyrinth of Thought. A History of Set Theory and its Role in Modern Mathematics, Birkhäuser, Ba­sel 2007.

(5) Löwen­he­im L., Über Möglichkeiten im Re­la­tiv­kalkül, Mathematische Annalen, Vol. 76, 1915. 6 Za vi­še o ovoj te­mi, vi­di: Ba­de­sa C., The Birth of Model Theory: Löwenheim’s Theorem in the Frame of the Theory of Relatives, Prin­ce­ton Uni­ver­sity Press, Prin­ce­ton 2004.

(7) Isti­ni za vo­lju, zna­čaj for­ma­li­za­ci­je arit­me­ti­ke ni­je bio uočen isto­vre­me­no sa Hil­ber­to­vim na­vo­đe­njem po­me­nu­tog pro­ble­ma na svet­skom kon­gre­su ma­tema­ti­ča­ra. Ne­ko­li­ko go­di­na na­kon kon­gre­sa, Hil­bert nu­di iz­ve­sne na­zna­ke u po­gle­du to­ga ka­ko bi tre­ba­lo iz­gle­da­ti re­še­nje ovog pro­ble­ma, da bi tek dvade­se­tih go­di­na pro­šlog ve­ka for­mu­li­sao raz­vi­jen si­stem for­mal­ne arit­me­ti­ke unu­tar ko­ga ovo pi­ta­nje do­bi­ja jed­no sa­svim pre­ci­zno zna­če­nje.

(8) Či­ta­o­ca ko­ji bi že­leo da se bli­že upo­zna sa Hil­ber­to­vim pro­ble­mi­ma, kao i nekim re­še­nji­ma onih ko­ji su za lo­gi­ku po­seb­no va­žni, upu­ću­je­mo na ve­o­ma lep pre­gled: Mi­jaj­lo­vić Ž., Mar­ko­vić Z. i Do­šen K., Hilbertovi problemi i logika, Za­vod za udž­be­ni­ke i na­stav­na sred­stva, Be­o­grad 1986.

(9) Vi­di: Gödel K., Über for­mal unentsche­id­ba­re Sätze der Principia Mathematica und ver­wand­ter Syste­me I., Monatshefte für Mathematik und Physik, Vol. 38, 1931.

(10) Iz­ve­sna do­za opre­za je neo­p­hod­na na ovom me­stu. Ni­je u pot­pu­no­sti ja­sno ko­ja se tač­no sred­stva mo­gu sma­tra­ti fi­ni­ti­stič­kim. Naj­če­šće se pret­po­sta­vlja da je, za Hil­ber­ta, fi­ni­ti­stič­ki frag­ment for­mal­ne arit­me­ti­ke oli­čen u Sko­lemovoj primitivno-rekurzivnoj aritmetici (PRA). Uko­li­ko je ovo slu­čaj, on­da za­i­sta PRA ne do­ka­zu­je kon­zi­stent­nost for­mal­ne arit­me­ti­ke na osno­vu dru­ge Ge­de­lo­ve te­o­re­me o ne­pot­pu­no­sti. Me­đu­tim, ova­kvo od­re­đe­nje fi­ni­ti­stič­ki do­pu­šte­nih sred­sta­va se mo­že sma­tra­ti pre­stro­gim. Ta­ko, uko­li­ko do­pu­sti­mo iz­ve­sne ob­li­ke tran­sfi­nit­ne in­duk­ci­je u kor­pu­su fi­ni­ti­stič­kih sred­sta­va, mo­gu­ će je da­ti po­tvr­dan od­go­vor na Hil­ber­tov dru­gi pro­blem.

(11) Gent­zen G., Die Wi­der­spruchsfre­i­he­it der re­i­nen Za­hlent­he­o­rie, Mathematische Annalen, Vol. 112, 1936.

(12) Gent­zen G., Be­we­is­bar­ke­it und Un­be­we­is­bar­ke­it von Anfangsfällen der transfi­ni­ten In­duk­tion in der re­i­nen Za­hlent­he­o­rie, Mathematische Annalen, Vol. 119, 1943. Re­zul­ta­ti ob­ja­vlje­ni u ovom ra­du deo su Gen­ce­no­ve ha­bi­li­ta­ci­o­ne te­ze, od­bra­nje­ne 1939. go­di­ne.

(13) Ka­ko smo već na­po­me­nu­li, Gen­cen je bio Ber­naj­sov đak, ali je for­mal­ni men­tor nje­go­ve dok­tor­ske di­ser­ta­ci­je bio Her­man Vajl. Raz­log ovo­me je­ste to što je Ber­naj­su 1933, zbog nje­go­vog je­vrej­skog po­re­kla, od­u­ze­ta pro­fe­su­ra u Ge­tin­ge­nu.

(14) Te­za je ob­ja­vlje­na u dva de­la i to kao: Gent­zen G., Un­ter­suc­hun­gen über das lo­gische Schließen I, Mathematische Zeitschrift, Vol. 39, 1934. i Un­ter­suchun­gen über das lo­gische Schließen II, Mathematische Zeitschrift, Vol. 39, 1935. U prevodu na engleski jezik: “Investigations into logical deduction”, in: Szabo M. E. (ed.), The Collected Papers of Gerhard Gentzen, NorthHolland, Amsterdam, 1969.

(15) Ak­ce­nat je ov­de ko­li­ko na sa­mom do­ka­zu, to­li­ko, ako ne i vi­še, na for­mu­laci­ji. Či­ni se da je ste­pen ori­gi­nal­no­sti ko­ji je Gen­cen po­ka­zao bio neo­p­ho­dan da bi se spro­ve­la pra­va ana­li­za lo­gič­ke de­duk­ci­je i, na­kon to­ga, uop­šte formu­li­sa­la po­me­nu­ta te­o­re­ma. Ne­što slič­no do­go­di­lo se ne­ko­li­ko go­di­na ra­ni­je, 1930. go­di­ne, ka­da je Ge­del do­ka­zao teoremu potpunosti pre­di­kat­skog ra­čuna, jed­nu od naj­va­žni­jih te­o­re­ma lo­gi­ke uop­šte. Svi neo­p­hod­ni re­zul­ta­ti bi­li su ta­ko­re­ći „u va­zdu­hu“, ali ni­ko se­bi ni­je po­sta­vio to pi­ta­nje.

 (16) Ka­ko već sa­mo ime go­vo­ri, po­jam Tju­rin­go­ve ma­ši­ne du­gu­je­mo en­gle­skom lo­gi­ča­ru Ale­nu Tju­rin­gu, ko­ji ga je for­mu­li­sao 1935, kao dva­de­set­dvo­go­di­ šnji stu­dent ma­te­ma­ti­ke na Uni­ver­zi­te­tu u Kem­bri­džu. Tju­rin­gov rad, ob­javljen na­red­ne, 1936. go­di­ne, je­dan je od ka­me­na te­me­lja­ca te­o­ri­je iz­ra­čun­ljivo­sti, ve­ro­vat­no i naj­zna­čaj­ni­ji. U ovom ra­du Tju­ring nu­di ve­o­ma pre­ci­znu ana­li­zu poj­ma in­tu­i­tiv­ne iz­ra­čun­lji­vo­sti, da bi u sve­tlu ove ana­li­ze for­mu­li­sao po­jam Tju­rin­go­ve ma­ši­ne, ve­o­ma jed­no­stav­nog, for­mal­nog mo­de­la (in­tu­itiv­ne) iz­ra­čun­lji­vo­sti. Po­red to­ga, Tju­ring je de­fi­ni­sao po­jam ta­ko­zva­ne univerzalne Tjuringove mašine, ko­ja je u sta­nju da opo­na­ša rad ma ko­je dru­ge Tju­rin­go­ve ma­ši­ne. Na kra­ju, Tju­ring je do­ka­zao i neo­d­lu­či­vost pre­di­kat­skog ra­ču­na, da­ju­ći pri­tom (ne­ga­ti­van) od­go­vor na Hil­ber­tov Entscheidungsproblem. Vi­di: Tu­ring A., On Com­pu­ta­ble Num­bers, with an Ap­pli­ca­tion to the Entsche­i­dung­spro­blem, Proceedings of the London Mathematical Society. Second Series, Vol. 42, 1936.

(17) Po­jam re­kur­ziv­ne funk­ci­je pr­vi uvo­di Ge­del, u ra­du iz 1931. u kom je do­kazao svo­je te­o­re­me o ne­pot­pu­no­sti. Ne­du­go za­tim, ovaj po­jam je stan­dar­dizo­vao Ste­fan Kol Kli­ni (Step­hen Co­le Kle­e­ne), da­ju­ći mu ob­lik u ko­me ga i da­nas za­ti­če­mo. Vi­di: Kle­e­ne S. C., Ge­ne­ral re­cur­si­ve fun­cti­ons of na­tu­ral num­bers, Mathematische Annalen, Vol. 112, 1936, kao i Re­cur­si­ve pre­di­ca­tes and qu­an­ti­fi­ers, Transactions of the American Mathematical Society, Vol. 53, 1943. istog auto­ra.

(18) Lamb­da-de­fi­na­bil­ne funk­ci­je pr­vi put uvo­di ame­rič­ki lo­gi­čar Alon­zo Čerč (Alon­zo Church) u ra­du An un­sol­va­ble pro­blem of ele­men­tary num­ber theory, American Journal of Mathematics, Vol. 58, 1936. U ovom ra­du Čerč je, na­za­vi­sno od Tju­rin­ga, do­ka­zao ne­re­ši­vost Hil­ber­to­vog Entscheidungsproblem-a.

(19) Po­jam Po­sto­ve ma­ši­ne du­gu­je­mo ame­rič­kom lo­gi­ča­ru polj­skog po­re­kla, Emi­lu Po­stu (Emil Post), ko­ji ga je for­mu­li­sao u ra­du Fi­ni­te Com­bi­na­tory Pro­ces­ses. For­mu­la­tion I, The Journal of Symbolic Logic, Vol. 1, 1936.

(20) Svi kla­sič­ni ra­do­vi iz te­o­ri­je iz­ra­čun­lji­vo­sti ko­je smo do sa­da ima­li pri­li­ke da na­ve­de­mo, sa­bra­ni su u zbor­ni­ku: Da­vis M., The Undecidable. Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Ra­ven Press, New York 1965.