Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

The quest for a most general framework supporting universal reasoning is very prominently represented in the works of Leibniz. He envisioned a scientia generalis founded on a characteristica universalis, that is, a most universal formal language in which all knowledge about the world and the sciences can be encoded. A quick study of the survey literature on logical formalisms suggests that quite the opposite to Leibniz’ dream has become reality. Instead of a characteristica universalis, we are today facing a very rich and heterogenous zoo of different logical systems, and instead of converging towards a single superior logic, this logic zoo is further expanding, eventually even at accelerated pace. As a consequence, the unified vision of Leibniz seems farther away than ever before. However, there are also some promising initiatives to counteract these diverging developments. Attempts at unifying approaches to logic include categorial logic algebraic logic and coalgebraic logic.

My own research draws on another alternative at universal logical reasoning: the shallow semantical embeddings (SSE) approach. This approach has a very pragmatic motivation, foremost reuse of tools, simplicity and elegance. It utilises classical higher-order logic [21] as a unifying meta-logic in which the syntax and semantics of varying other logics can be explicitly modeled and flexibly combined (cf. [3] and the references therein). Off-the-shelf higher-order interactive and automated theorem provers [6] can then be employed to reason about and within the shallowly embedded logics.

Respective experiments have e.g. been conducted in metaphysics. An initial focus thereby has been on computer-supported assessments of modern variants of the ontological argument for the existence of God, where the SSE approach has been utilised in particular for automating variants of higher-order (multi-)modal logics [8].

In the course of these experiments (cf. [13,14,15,16,17,18] for details), my prover LEO-II [9] detected an previously unnoticed inconsistency in Kurt Gödel’s [25] prominent variant of the ontological argument, while the slightly modified variant by Dana Scott [31] was verified in the interactive proof assistants Isabelle/HOL [29] and Coq [19]. Further modern variants of the argument have subsequently been studied with the approach, and theorem provers have even contributed to the clarification of an unsettled philosophical dispute [12].

Another, more ambitious study has focused on Ed Zalta’s Principia Logico-Metaphysica (PLM) [37], which aims at a foundational logical theory for all of metaphysics and the sciences. This includes mathematics, and in this sense it is more ambitious than Russel’s Principia Mathematica. The semantical embedding of PLM in HOL has been very challenging, since in addition to its size, its foundational theory is complicated: the PLM is based on hyperintensional higher-order modal logic S5 defined on top of a relational (as opposed to a functional) type theory that comes with restricted comprehension principles (the use of full comprehension in the PLM has been known to cause paradoxes and inconsistencies [30]). The PLM has meanwhile been successfully encoded in Isabelle/HOL by my student Daniel Kirchner [26]. As an unexpected highlight of this project, Kirchner, supported by the Isabelle/HOL system, detected an previously unnoticed issue: a deeply rooted and known paradox is reintroduced in PLM when the logic of complex terms is adjoined to PLM’s specially-formulated comprehension principle for relations. Kirchner is now using the framework to support Zalta in fixing this issue.

Other logics, for which the SSE approach applies, and which are relevant for theoretical philosophy, include quantified conditional logics and multi-valued logic [4, 5, 34].

Motivated by the successful experiments on the ontological argument, and supported by my research group at Freie Universität (FU) Berlin, I have set-up a worldwide new lecture course on computational metaphysics [36], which has received FU Berlin’s central teaching award in 2015/16. Student projects originating from this course have led to impressive new contributions (cf. [1, 24, 26]; further papers are submitted), including Kirchner’s already mentioned embedding of the PLM in HOL, a computer-assisted reconstruction of an ontological argument by Leibniz and a verification of (main parts of) prominent textbooks by Fitting [22] and Boolos [20]. A key factor in the successful implementation of the course has been, that a single methodology and overall technique (the SSE approach) was used throughout, enabling the students to quickly adopt a wide range of different logic variants in short time within a single proof assistant (Isabelle/HOL). The course concept seems in fact well suited to significantly improve interdisciplinary, university level logic education.

Another interesting application area for the SSE approach is mathematics, where e.g. the proper treatment of partiality and undefinedness in computer-formalisations constitute unsettled challenges. Free logic [28, 32] adapts classical logic in a way particularly suited for addressing them. Free logics have interesting applications, e.g. in natural language processing and as a logic of fiction. In mathematics, free logics are particularly suited in application domains such as category theory or projective geometry (e.g. morphism composition in category theory is a partial operation). In a collaboration with Dana Scott, I have shown that free logics can be elegantly embedded and automated in HOL [10]. Utilising this embedding, we have conducted an exemplary theory exploration study in category theory [11], in the course of which theorem provers have revealed a previously unnoticed technical flaw (constricted inconsistency resp. missing axioms) in a prominent category theory textbook [23].

The SSE approach is, of course, relevant also for artificial intelligence and computer science. For example, the knowledge and belief of intelligent agents can be modelled with epistemic and doxastic logics, which are directly amenable to the SSE approach, since they are just particular modal logics. To demonstrate this, prominent AI puzzles about knowledge and belief, including the well known wise men puzzle, have been successfully automated [3, 35]. Moreover, the semantic web description logic ALC is just a reinvention of basic multi-modal logic K and, hence, the SSE approach is immediately applicable to it. Access control logics have applications e.g. in computer security; again the SSE approach applies [2]. Further ongoing work e.g. adresses intuitionistic modal logic [27] and predicate dynamic logic.

In summary, the SSE approach is the most widely applied universal logical reasoning approach to date. Note, however, the difference to Leibniz’ original idea (and to various strands of related work). Instead of a single, universal logic formalism, the SSE approach supports many different competing object logics from the logic zoo. No ontological commitment is thus enforced at the object logic level (e.g. the approach well supports both classical and intuitionistic object logics, and can even combine them [7]). The concrete selection of (a range of) object logic candidates is typically determined by the specific requirements of the application at hand. Only at meta-level a single, unifying logic is provided, namely HOL (or any richer logic incorporating HOL). By unfolding the embeddings of the object logics, problem representations are uniformly mapped to HOL. This way Leibniz’ vision is realised in an indirect way: universal logical reasoning is established (only) at the meta-level in HOL.