Interview: Christoph Benzmueller ... potom počítač dokázal: Boh existuje

Minuloročný článok "Gödelov dôkaz existencie Boha potvrdený" o automatizovanom-strojovom dokazovaní existencie Boha matematikmi Christophom Benzmuellerom a Brunom Paleom zaujal veľký počet našich čitateľov. Dnes sa k tejto téme vraciame a pozrieme sa na ňu omnoho podrobnejšie.

Interview: Christoph Benzmueller  ... potom počítač dokázal: Boh existuje (slovenská verzia)

Pred pár mesiacmi sa na arXiv.org objavil odborný článok o automatizovanom dokazovaní existencie Boha. Nasledujúci rozhovor s jedným z jeho autorov Christophom Benzmuellerom je o tom ako s Brunom Paleom potvrdili správnosť Gödelovho dôkazu existencie Boha.

Mohli by ste nám podrobne priblížiť čím sa zaoberá Váš článok?

Kurt Gödel (1906-1978) navrhol argumentačný formalizmus dokazujúci existenciu Boha. Pokusy dokázať existenciu (alebo ne-existenciu) Boha vo význame ontologického argumentu sú starou tradíciou v západnej filozofii. Už pred Gödelom viacerí filozofi, vrátane Sv. Anselma, Descarta a Leibnitza zverejnili podobné argumenty. Čo motivovalo Gödela ako logika, bola otázka, či je možné odvodiť existenciu Boha z malého množstva základných axióm a definícií, matematicky presným a logicky formálnym argumentačným reťazcom.

Čo sme s Brunom Woltzenlogel Paleom z TU Vienna spravili, bola formalizácia Kurt Gödelovho argumentu pre existenciu Boha na počítači a jeho automatické dokázanie. Z Gödelových premís, potom počítač dokázal: Boh existuje. "Automatizované dokazovanie teorém" je matematická disciplína kde sú vyvíjané takéto automatizované systémy. Zaujímavé bolo, že dokazovateľ teorém (pozn. red. automatický program) našiel aj niekoľko nových výsledkov týkajúcich sa Gödelovho argumentu.

Formálne logické konfrontácie s takýmito dôkazmi Božej existencie boli v teoretickej filozofii doteraz (zväčša) limitované na použitie papiera a pera. Použitiu počítačov doteraz bránilo to, že "logika" dostupných systémov dokazovania teorém nebola dostatočne expresívna (schopná vyjadriť) na adekvátne formulovanie významu konceptov. Gödelov dôkaz napríklad používa komplexnú modálnu logiku vyššieho rádu na narábanie s konceptmi ako "možné" a "nutné" pre podporu kvantifikácií cez jednotlivosti a vzťahy.

Aktuálne naša spoločná práca s Larry Paulsonom z Cambridge University UK ukazuje, že veľa expresívnych logík, vrátane modálnych logík vyšších rádov, môže byť zahrnutých do klasickej logiky vyššieho rádu, ktorá tak môže byť videná ako univerzálna logika. Pre túto univerzálnu logiku boli v posledných rokoch vyvinuté efektívne automatické dokazovače teorém a tieto systémy boli využité v našej práci.
 

Kedy Vás napadlo zaoberať sa ontologickým dôkazom takýmto automatizovaným spôsobom?

Táto myšlienka bola pre mňa výzvou už približne 6 rokov. Bola to kniha Melvina Fittingsa "Types, Tableaus, and Gödel's God", ktorá pôvodne vzbudila môj záujem. V posledných rokoch som pracoval na zahrnutí rôznych expresívnych logík do klasickej logiky vyššieho rádu. Mojím hlavným cieľom teda bola podpora vylepšenej technológie uvažovania pre rôzne aplikácie, napríklad pre umelú inteligenciu. Tento výskum tiež vydláždil cestu pre spútanie ontologického dôkazu s počítačovou technológiou. Koncom roka 2012 som pri prezentácii tohto výskumu pre Spoločnosť Kurta Gödela vo Viedni stretol Bruna Woltzenlogela Paleoa. Bruno sa veľmi zaujímal o formalizáciu ontologického argumentu z osobných dôvodov (koncom roku 2012 prechádzal ťažkým obdobim) a chcel prezentovať formalizáciu Gödelovho ontologického dôkazu ako dar pre kňaza doma v Brazílii. Potom ma začiatkom roku 2013 kontaktoval a rozhodli sme sa spoločne pracovať na formalizácii a automatizovaní ontologického argumentu. Od úplného začiatku nám bolo obom celkom jasné, že počítačovo-založená formalizácia a automatizácia Gödelovho ontologického argumentu patrí z rôznych dôvodov medzi významné vedecké otázky. Pripomeňme si, že takýto výpočtový pohľad na filozofiu bol načrtnutý už Leibnitzom.


Ako dlho ste pripravovali článok? Je za tým nejaký príbeh?

Vlastne áno, pričom časť príbehu bola spomenutá vyššie. Boli sme úspešní pri prvom automatickom dôkaze verzie Gödelovho ontologického argumentu od Dana Scotta začiatkom júla 2013, a bol to LEO II, môj vlastný dokazovateľ teorém vyššieho rádu, ktorý to dokázal ako prvý. Následne sme zopakovali výsledky s inými systémami. Na úplnom začiatku som si nebol istý akú publikačnú stratégiu by sme mali zvoliť. Bruno ma presvedčil, že uploadnutie celej našej práce na GitHub bude najlepším spôsobom ako pokračovať.

Raul Rojas z Freie Universität, ktorému som krátko povedal o našej úspešnej práci ma potom požiadal o interview pre Telepolis/Heise. V rovnakom čase sme zaslali dvojstránkový článok do arXiv aby sme mali k dispozícii prvú referenciu. Samozrejme, v blízkej budúcnosti zverejníme ďalšie publikácie; prvá sa už objavila: http://afp.sourceforge.net/entries/GoedelGod.shtml . Ďalšie sú zaslané. Tieto budúce články vysvetlia náš výskum a jeho dôsledky do väčšej hĺbky rôznym cieľovým komunitám.
 

Aké boli reakcie po zverejnení článku? Bolo ich veľa?

Áno, silné reakcie. Konkrétne, Telepolis interview a články v Spiegel Online spustili silné reakcie. Telepolis interview skončilo medzi ich desiatimi najčítanejšími článkami v roku 2013. Predpokladám, že podobné to bude pri niektorých ďalších správach o našej práci. Mnohé reakcie boli skôr iracionálne a často odhalili nedostatok vedomostí čitateľov o prírode a úlohe ontologického argumentu vo filozofii a teológii, alebo ukázali nedostatok vedomostí o formálnej logike a dokazovaní teorém. Ďalšie reakcie boli veľmi zaujímavé a inšpirujúce. Dostali sme aj veľmi cenné odozvy od profesionálnych filozofov, s ktorými sme začali mimoriadne plodnú diskusiu. Naviac sme boli kontaktovaní biskupom rímskokatolíckej cirkvi, s ktorým sa Bruno stretol vo Viedni.

Boli medzi reakciami nejaké kuriózne?

Áno, objavili sa mnohé vtipné komentáre z diskusných fór rôznych webstránok, ktoré informovali o našej práci. Tiež ma kontaktovalo zopár ľudí, ktorí mi prezentovali ich vlastné teórie o hlavných a fundamentálnych otázkach o svete a Bohu. Bohužiaľ, nemám zdroje a čas komentovať všetky tieto ohlasy. Často musím odpovedať, že mojimi hlavnými záujmami (doteraz) boli čisto logické aspekty ontologického argumentu.


Zverejnili ste riešenie na GitHub vo forme open source projektu. Evidujete zapojenie sa komunity do riešenia projektu?

Bohužiaľ takéto štatistické údaje sú aktuálne prístupné len na GitHub. To je škoda, rád by som tieto čísla tiež poznal. Hoci, od mnohých študentov na mojej univerzite viem, že si zdrojáky stiahli a pracovali s nimi. Najnovšie ma niektorí študenti kontaktovali so zaujímavými komentármi a prácami. Vo všeobecnosti, chceme pozvať výskumníkov z celého sveta ktorých to zaujíma, aby sa zapojili do našej iniciatívy. Nanešťastie na celkové ovládnutie kódu je potrebné značné množstvo logického tréningu.


Veríte v Boha? Aká je Vaša pozícia v tejto otázke?

Vyrastal som v nábožensky založenej rodine; a teda moje zázemie môže byť označené ako religiózne. No ako vedec som si vyvinul čisto racionálny prístup, aj čo sa týka fundamentálnych otázok diskutovaných vyššie. V skutočnosti, moja osobná viera nehrala a nehrá úlohu v našej práci na Gödelovom ontologickom argumente. Hnacím momentom bol skôr hlboký záujem o logické zvláštnosti Gödelovho dôkazu a tiež moja rastúca fascinácia o oblasť metafyziky. Musím ale priznať, že sa prikláňam v pozitívnej odpovedi na otázku existencie Boha. Nanešťastie, Gödelov dôkaz sa mi nezdá celkom presvedčivý, keďže existuje niekoľko oprávnených námietok ohľadom niektorých jeho axióm. Veľmi zaujímavou otázkou je či technológia môže pomôcť pri ďalšej analýze a vylepšení argumentu.


Na akých témach/projektoch momentálne pracujete?

V súčasnosti pracujem na štyroch prepojených výskumných smeroch:

• Pred šiestimi rokmi som začal študovať ako môže byť rozšírená klasická logika vyššieho stupňa využivaná ako univerzálna logika. Základnou myšlienkou je zahrnúť iné sľubné logiky do klasickej logiky vyššieho rádu a aplikovať na ne automatizovaný dokazovateľ teorém. Modálna logika vyššieho stupňa požadovaná v Gödelovom ontologickom argumente je len jedným príkladom. Iná, ešte zaujímavejšia logika, ktorá môže byť ľahko zahrnutá je kondicionálna logika vyššieho stupňa. Tiež bezpečnostné logiky môžu byť automatizované týmto spôsobom. A najzaujímavejšie, kombinácia týchto logík alebo dokonca častí ich meta-teórií môže byť formalizovaná a automatizovaná.
• Spolu so skupinou študentov som začal re-implementáciu môjho dokazovateľa teorém LEO II; Práve som získal financovanie z German National Research Foundation (DFG) pre realizáciu tohto zámeru. Nový systém nazveme LEO-III. V ideálnom prípade chcem optimalizovať LEO-II pre automatizáciu logických zahrnutí, vrátane logík ako je potrebné pre automatické argumentovanie v teoretickej filozofii.
• Spolu s Brunom Woltzenlogel Paleom chcem formalizovať rozsah rôznych variácií ontologického argumentu. Radi by sme formalizovali hlavné časti učebnice Sobel "Logic and Theism". Naviac, chceme sa pokúsiť o ďalšie vylepšenie Gödelovho ontologického argumentu. Aktuálne sa pokúšame zabezpečiť financovanie pre tento projekt.
• V záujme vytvorenia väčšej komunity potrebujeme výrazne zlepšiť užívateľské rozhranie našich argumentačných nástrojov. Doteraz sú vhodné len pre expertov. V ideálnom prípade by sme radi vyvinuli výkonný a jednoducho používateľný argumentačný framework (prostredie) pre aplikácie v teoretickej filozofii. To je ďalší výskumný smer pre ktorý by sme radi získali financovanie a vytvorili silný tím.

Christoph Benzmüller je počítačový vedec, matematik a filozof pracujúci na Freie Universität Berlin. Aktuálne bol ocenený Heisenbergovým Fellowship-om od Nemeckej Národnej Výskumnej Nadácie (German National Research Foundation - DFG) a nominovaný na cenu Amalia Preis für Neues Denken. Študoval a pracoval na rôznych svetových univerzitách vrátane Cambridge, Edinburgu a Birminghamu vo Veľkej Británii, Carnegie Mellon University v USA, a Saarland University v Nemecku. Pred akademickou kariérou bol nemeckým národným šampiónom v behu na dlhé vzdialenosti.