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.

 

 

Interview: Christoph Benzmueller  ... the computer then proved: there exists God (in english)

The next interview with Christoph Benzmueller is about his way to God existence Gödel ontological proof automated proving. Few months ago together with Bruno Woltzenlogel Paleo published an article at arxiv.org about their work. 

Could you please, explain the main idea and results of your article?

Kurt Gödel (1906-1978) proposed an argumentation formalism to prove the existence of God. Attempts to prove the existence (or non-existence) of God by means of abstract, ontological arguments are an old tradition in western philosophy. Before Gödel, several well known philosophers, including St. Anselm, Descartes and Leibniz, have presented similar arguments. What motivated Gödel as a logician was the question, whether it is possible to deduce the existence of God from a small number of foundational axioms and definitions, with a mathematically precise and logically formal argumentation chain.

What Bruno Woltzenlogel Paleo from TU Vienna and I did was to formalize Kurt Gödel's argument for God's existence on a computer and to verify it automatically. From Gödel's premises, the computer then proved: there exists God. "Automated theorem proving" is the mathematical discipline where such automated systems are developed. Interestingly, the theorem provers also found some new results about Gödel's argument.

In theoretical philosophy, formal logical confrontations with such proofs of God's existence had been so far (mainly) limited to paper and pen. Up to now, the use of computers was prevented, because the "logics" of the available theorem proving systems were not expressive enough to formalize the abstract concepts adequately. Gödel's proof uses, for example, a complex higher-order modal logic to handle concepts such as "possible" and "necessary" and to support quantification over individuals and properties.

Current works of myself and Larry Paulson from Cambridge University, UK, show that many expressive logics, including higher-order modal logics, can be embedded into the classical higher-order logic, which can thus be seen as a universal logic. For this universal logic, efficient automated theorem provers have been developed in recent years, and these systems were now employed in our work.

When did you get the idea to work on Gödels ontological proof in "automated way"?

I have been challenged by the idea since about 6 years. It was actually Melvin Fittings book on "Types, Tableaus, and Gödel's God" that initially raised my interest. In the last few years I have then been working on embeddings of various expressive logics in classical higher-order order logics. My main goal thereby was to support improved reasoning technology for various applications, for example, in artificial intelligence. But clearly, this research also paved the way for tackling the ontological argument with computer technology. End of 2012, I then met Bruno Woltzenlogel Paleo in Vienna, where I presented this research to the Kurt Gödel society. Bruno was highly interested in formalizing the ontological argument for personal reasons (he went though some very hard time end of 2012), and he wanted to present a formalization of Gödel's ontological proof as a gift to a priest back home in Brazil. He then contacted me in early 2013 and we decided to jointly work on the formalization and automation of the ontological argument. From the very beginning it was very clear to both of us, that the computer-based formalization and automation of Gödel's ontological argument was of major scientific interest for various reasons. Most importantly, we provide a significant novel contribution towards a computer-supported theoretical philosophy. Remember that such a computational view on philosophy was already pictured by Leibniz.


Is there a story behind creation of the article/code?

Well, yes, and part of the story has already been mentioned above. We succeeded with the first automated proof of Dana Scott's version of Gödel's ontological argument in early July 2013, and it was actually LEO-II, my own higher-order theorem prover, which did prove the result first. Subsequently we reproduced the results with other systems. At the very beginning, I wasn't sure which publishing strategy we should follow. Bruno convinced me that uploading our entire work on GitHub would be the right way to proceed. Raul Rojas at Freie Universität Berlin, whom I had briefly told about our successful work, then prepared the Telepolis/Heise interview with me. And at the same time we did submit the two page article to the arXiv repository in order to have a first reference available. We will, of course, add further publications in the near future; one has already appeared: http://afp.sourceforge.net/entries/GoedelGod.shtml. Others are submitted. These future papers will explain our work and its implications in more depth to different target communities.


What were the reactions after publishing? Were there a lot of them?

Yes, there were strong reactions. In particular, the Telepolis interview and the Spiegel Online article(s) triggered such strong reactions. In fact, the interview on Telepolis was amongst their top ten most read articles in 2013. I assume that a similar statement can be made for some other reports on our work. Many of the reactions to our work were rather irrational, and often they revealed a lack of knowledge in the readers about the nature and role of the ontological argument in philosophy and theology, or they showed a lack of knowledge about formal logic and theorem proving. Other reactions were highly interesting and inspiring. We also got some highly valuable feedback from expert philosophers, and we have started some very fruitful discussions with them. Moreover, we got contacted by a bishop from the roman catholic church, and Bruno met him in Vienna.

Were there also funny or surprising ones?

Well, yes, there are many funny forum comments on the various websites that reported on our work. I also got contacted by several people who presented me their own theories on essential and fundamental questions about the world and about God. Unfortunately, I do not have the resources and the time to comment on all of these requests. Often I have to respond to them that my core interests (so far) have been on the pure logical aspects of the ontological argument.


The project was published at GitHub in open source form. Did many people download (/use) your code? Did somebody modify it in any way? Is there some contribution of community actually?

Unfortunately such statistics data has only recently been made available on GitHub as it seems. This is pity, and I would actually like to know these numbers as well. However, I know from many students at my university that they have downloaded the sources and worked with them. Some students have recently contacted me with some interesting comments and developments. Generally, we would like to invite interested researchers worldwide to join our initiative. Unfortunately, there is still a fair amount of logic training required to fully master the code.


Do you, personally, believe in God? What is your position in this field?

I grew up in a religious family; thus my background can be classified as religious. As a scientist, however, I have developed a purely rational attitude, also regarding fundamental questions as we discuss them here. In fact, my personal belief didn't and doesn't play a role in our work on Gödel's ontological argument. The driving element for me has rather been a deep interest in the logical peculiarities of Gödel's proof and also my growing fascination for the field of metaphysics. But I have to admit that I am in favor of a positive answer to the question of the existence of God. Unfortunately, however, Gödel's proof appears not yet fully convincing to me, since there is some justified criticism regarding some of his axioms. A very interesting question now is whether our technology can eventually help to further analyze and improve the argument.


What topics or subjects are you currently working on and/or planing to work on in the future?

I am currently working on basically four interconnected research directions:

• Six years ago I have started studying to what extent classical higher-order logic can be exploited as a universal logic. The idea is to embed other challenging logics in classical higher-order logics and to apply higher-order automated theorem provers to them. Higher-order modal logic, as required in Gödel's ontological argument, is just one example. Another, even more interesting logic that can be easily embedded is higher-order conditional logic. Also security logics can be automated this way. And most interestingly, combinations of these logics and even parts of their meta-theory can be formalized and automated.
• Together with a group of students I am about to start a re-implementation of my LEO-II theorem prover; I just received some funding from the German National Research Foundation (DFG) to carry out this project. The new system will be called LEO-III. Ideally, I want to optimize LEO-III for the automation of logic embeddings, including the logics as required for automating arguments in theoretical philosophy.
• Together with Bruno Woltzenlogel Paleo I want to formalize a range of variations of the ontological argument. In fact, we would like to formalize major parts of the textbook by Sobel on "Logic and Theism". Moreover, we want to try to further improve Gödel's ontological argument. Currently we try to raise funds for such a project.
• In order to create a larger community we need to significantly improve the user interfaces of our reasoning tools. So far they are suitable only to expert users. Ideally, we should develop a powerful and easy to use reasoning framework for applications in theoretical philosophy. This is another research direction for which I would like to raise funds and create a strong team.

Christoph Benzmüller is Computer Scientist, Mathematician and Philosopher working at Freie Universität Berlin. Recently he got awarded a Heisenberg Fellowship of the German National Research Foundation (DFG) and he was nominated for the Amalia Preis für Neues Denken. He studied and worked at various international universities, including Cambridge, Edinburgh and Birmingham in the UK, Carnegie Mellon University in the US, and Saarland University in Germany. Previous to his academia career he was a German national champion in long distance running.