Professor of Freie Universität Berlin made his presence felt in event that marked the transition to School of Technology
Christoph Benzmüller
The final activity in celebration of the School of Computer Science’s 40th anniversary featured Christoph Benzmüller, from Freie Universität Berlin and Saarland University, Saarbrücken, both in Germany. The event will also marked the Computer Science program’s transition to the School of Technology of PUCRS.
In his two lectures What has the Mechanisation of Category Theory in Common with Proving God’s Existence? and Automated Reasoning in Higher-order and Non-classical Logics, Benzmüller addressed topics such as theoretical computer fundamentals and supporting computer tools for the construction of deductive systems; the interdisciplinary potential of Computer Science beyond the use of computer apparatus; and several variations of Gödel’s ontological argument for the existence of God that have been analyzed with computer-automated tools.
Today, Benzmüller is a visiting professor at the University of Luxembourg. He has conducted research in institutions such as Stanford University (EUA), University of Cambridge, University of Birmingham e University of Edinburgh (Inglaterra). Benzmüller gave us an interview as he talked about universal logic, metalogic approach and reasoning automation, among other things.
Interview
What is the importance of Logic (Mathematics) for Computer Science, Artificial Intelligence, Philosophy and other areas?
In these areas, logic has attracted a very special interest in (at least) two senses: (a) as a foundational tool enabling the rigorous modelling and analysis of theories, systems, processes, arguments, etc., and (b) as an object of study and continuous development itself. The term logic actually stands for many different logic formalisms that are existent today and which have been developed in these areas to support particular kind applications.
How can we apply logic to other areas such as Philosophy?
Many logic formalisms actually have their roots and their original motivation in theoretical philosophy and metaphysics. Computer scientists, in particular, do sometimes forget about this. In my ongoing work, I am applying theorem provers, that is, computer systems that automate logical reasoning, for the rigorous and critical analysis of prominent arguments in philosophy, for example, the ontological argument for the existence of God. In our experiments, theorem provers have even contributed novel knowledge and detected flaws in human arguments.
The laymen usually do not realize the presence of Logic in their lives. Where else can we find it?
Logic is at the heart of rational argumentation, and rational argumentation is fundamental for our scientific and societal processes in general. Logic is thus important much beyond Philosophy, Computer Science, and AI. Unfortunately, rationality seems slightly in decline in recent years, e.g. in some political debates worldwide. This is very unfortunate, and it should be in our very deep interest to change this trend again.
Can you please describe the method used to prove Gödel’s ontological proof? In what other areas can it be applied? Can you give us examples?
The analysis of Gödel’s argument on the computer requires the prior implementation of variants of very expressive logic formalisms, so called higher-order modal logics. These logics support an adequate handling of the notions of necessity and possibility, which are important in this context. Variants of higher-order modal logics are generally very important for formalizations in metaphysics, which typically require a high degree of expressivity to adequately capture the complex notions and terms as they occur.
However, computer implementations of such rich logics is by no means trivial. In our work we use an indirect approach, that allows us to reuse existing theorem proving technology. They key idea is to employ classical higher-order logic as a meta logic, in which we then model and implement variants of higher-order modal logics. Then we employ the latter in a subsequent step for the modelling and analysis of the ontological argument.
This meta logical approach to universal reasoning can be applied in many other areas. Right now I am particularly interested to adapt this technique for the implementation of so called deontic logics, which are e.g. relevant for enabling machines to perform legal and ethical reasoning. So far very few deontic logic reasoners have been implemented.
How are your research interests related to the Automated theorem proving?
Automated theorem proving is at the very heart of my research interests. Together with my students Alexander Steen and Max Wisniewski at FU Berlin, I am currently developing the higher-order theorem prover Leo-III (http://page.mi.fu-berlin.de/lex/leo3/), and prior to that I have developed the prover Leo-II (http://page.mi.fu-berlin.de/cbenzmueller/leo/) in a project with Larry Paulson at Cambridge University, UK. These systems in turn serve as some of various backbone reasoners in our meta-logical approach to universal reasoning. However, I often utilize them indirectly via another system, the proof assistant system Isabelle/HOL, which comes with a more intuitive user-interface and which provides powerful bridges to external theorem provers, including my Leo-prover(s). Generally, I am benefitting a lot in my current research from the ongoing coalescence of theorem proving technology in modern higher-order proof assistants, in particular, in Isabelle/HOL. The automation support in the systems is currently rapidly improving, and that is of course very beneficial in applications as discussed before.
How important is a Universal Logic (as brought forth by Leibniz) that enables us to reflect upon any other logic?
Different applications, in particular across disciplines, often require very different logic formalisms. A convincing universal logic approach, in particular, a practically relevant one that could serve all these applications (as envisioned by Leibniz), is unfortunately not what we have come up with yet. This is quite unfortunate, since implementing and maintaining all the heterogeneous species in the existing logic zoo is of course very difficult and also resource intensive. It is thus not surprising that many species in this zoo exist on paper only and have never been implemented and applied in practice.
The meta logical approach to universal logical reasoning I am proposing is trying to overcome this situation. The core message is: While it might not be possible to come up with a universal “object” logic as envisioned by Leibniz, it might in fact be possible to have a universal meta logic in which we can model, analyze and apply the various species from the logic zoo. And, in this sense, this approach tries to offer an interesting answer to Leibniz’ challenge.
Can you please tell us about your current investigations?
I consider machine ethics as very topical challenge area for my research. The automation of non-trivial ethical and legal reasoning in machines seems to require the implementation of rich and powerful logic formalisms (e.g., modern deontic logics). I am currently studying whether the meta logical approach to universal logical reasoning does in fact scale for such logics and for their applications in machine ethics and machine law.
