Christoph Benzmueller

Gödel’s ontological proof for the existence of God – as an inference from the level of rational, logical structure to the level of being – was strongly influenced by Leibniz’s monadology, which is based on the Ur-Monade – God – conceived as absolutely infinite. Gödel defines God as the maximum of positive properties and he characterizes this maximum (of being) with his postulates implicitly as an ultrafilter structure. Using maximality as criterion we have compared the set of positive properties in Scott’s version of Gödel’s theistic theory with modified variants of it to see whether a maximum is still achieved, or not, and what effect this has on modal collapse. The motivation for these, typically weakened, variants of Gödel’s theistic theory has been to avoid modal collapse and the limited determinism associated with it, and to show that the necessary existence of God can still be proved with less strong axioms. A weakening of the maximality criterion of the ultrafilter structure imposed by Gödel’s (and Scott’s) postulates have thus been applied to the set of positive properties in order to allow for alternative models in which modal collapse does not hold. In these alternative models, however, the maximality criterion for the basic quantity of positive properties is abandoned, so that in them God as a “maximum” is not reached. We argue that this is contrary to Gödel’s intention, and that for his conception of God, maximality and absolute infinity are non-negotiable. What Gödel had in mind, as we argue here, was a holistic – absolutely infinite – view of the world, i.e. with modal collapse, but without limited determinism.

Forschungsaktivitäten in Richtung starker Künstlichen Intelligenz (KI) bzw. Artificial General Intelligence (AGI)Artificial General Intelligence (AGI)AGI (Artificial General Intelligence)haben aktuell stark an Fahrt aufgenommen. Ausgangspunkt sind dabei beachtliche Fortschritte vor allem im Bereich der datengetriebenen subsymbolischen KI (z. B. dem tiefen maschinellen Lernen), aber auch in der regelbasiertenKünstliche Intelligenz (KI)symbolischesymbolischen KI.Künstliche Intelligenz (KI)subsymbolischeMit solchen Aktivitäten im Einklang stehen sollte das Bestreben nach verantwortungsvoller KI, oder besser noch, nach sicherer KI. Selbst wenn eine starke KI (zumindest aus meiner Sicht) nicht unmittelbar absehbar ist, sollte diesem Aspekt größte Aufmerksamkeit geschenkt werden. Es ist nämlich insbesondere der unreflektierte Einsatz leistungsfähiger unvollkommener KI-Systeme in sehr kritischen Anwendungsgebieten (einschließlich des militärischen Bereichs), der zunehmend Anlass zur Sorge bereitet. In diesem Kapitel skizziere ich meine Position zu den Themen starke und sichere KI, führe dazu Äußerungen aus vorherigen eigenen Arbeiten zusammen und ergänze diese.

Die Autorinnen und Autoren präsentieren in diesem Buch Argumente, die die Unmöglichkeit des Reduktionismus aus philosophischer, naturwissenschaftlicher bzw. mathematisch-logischer Perspektive zu begründen suchen. Der Reduktionismus behauptet, dass Eigenschaften auch von komplexen Systemen vollständig auf ihre Bestandteile zurückgeführt werden können. Diese Position ist einflussreich, aber umstritten. Im Jahr 2019 hat der Kurt Gödel Freundeskreis einen Essaywettbewerb veranstaltet, um schlagende Argumente gegen den Reduktionismus zu finden. Unter den internationalen Teilnehmern waren neben weltweit führenden Forschern auch Wissenschaftler, die noch am Beginn ihrer Kariere stehen. Dieser Band versammelt die Beiträge der Preisträger und weitere ausgewählte Aufsätze. Aus dem Inhalt: · Kausalität als antireduktionistisches Hausmittel – Martin Breul · Reduktionismus im Diskurs – Hanna Hueske · Monads, Types, and Branching Time – Kurt Gödel’s approach towards a theory of the soul – Tim Lethen · The limits of reductionism: thought, life, and reality – Jesse M. Mulder · True or Rational? A Problem for a Mind-Body Reductionist – Michał Pawłowski · Why reductionism does not work – George F. R. Ellis · Physik ohne Reduktion – Rico Gutschmidt · Is there an Axiom for everything? – Jean-Yves Béziau · Unerklärliche Wahrheiten – Marco Hausmann · Gödel, mathematischer Realismus und Antireduktionismus – Reinhard Kahle.

We report on the mechanisation of (preference-based) conditional normative reasoning. Our focus is on Åqvist's system E for conditional obligation, and its extensions. Our mechanisation is achieved via a shallow semantical embedding in Isabelle/HOL. We consider two possible uses of the framework. The first one is as a tool for meta-reasoning about the considered logic. We employ it for the automated verification of deontic correspondences (broadly conceived) and related matters, analogous to what has been previously achieved for the modal logic cube. The equivalence is automatically verified in one direction, leading from the property to the axiom. The second use is as a tool for assessing ethical arguments. We provide a computer encoding of a well-known paradox (or impossibility theorem) in population ethics, Parfit's repugnant conclusion. While some have proposed overcoming the impossibility theorem by abandoning the presupposed transitivity of ‘better than’, our formalisation unveils a less extreme approach, suggesting among other things the option of weakening transitivity suitably rather than discarding it entirely. Whether the presented encoding increases or decreases the attractiveness and persuasiveness of the repugnant conclusion is a question we would like to pass on to philosophy and ethics.

A simplified variant of Gödel’s ontological argument is presented. The simplified argument is valid already in basic modal logics K or KT, it does not suffer from modal collapse, and it avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel. The variant presented has been obtained as a side result of a series of theory simplification experiments conducted in interaction with a modern proof assistant system. The starting point for these experiments was the computer encoding of Gödel’s argument, and then automated reasoning techniques were systematically applied to arrive at the simplified variant presented. The presented work thus exemplifies a fruitful human-computer interaction in computational metaphysics. Whether the presented result increases or decreases the attractiveness and persuasiveness of the ontological argument is a question I would like to pass on to philosophy and theology.

Over the past decade, variants of Gödel's ontological arguments have been critically examined using modern symbolic AI technology. Computers have unearthed new insights about them and even contributed to the exploration of new, simplified variants of the argument, which now need to be further investigated by theologians and philosophers. In this article, I provide a brief, informal overview of these contributions and engage in a discussion of the possible future role of AI technology for the rigorous assessment of arguments in theology and philosophy.

Three variants of Kurt Gödel's ontological argument, proposed by Dana Scott, C. Anthony Anderson and Melvin Fitting, are encoded and rigorously assessed on the computer. In contrast to Scott's version of Gödel's argument the two variants contributed by Anderson and Fitting avoid modal collapse. Although they appear quite different on a cursory reading they are in fact closely related. This has been revealed in the computer-supported formal analysis presented in this article. Key to our formal analysis is the utilization of suitably adapted notions of ultrafilters, and a careful distinction between extensions and intensions of positive properties.

Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects.This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms is simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics.Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics.

We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higher-order logics and aims at formalizing natural-language argumentative discourse using flexible combinations of expressive non-classical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on networks of structured arguments and is iterative and two-layered. At one layer we search for logically correct formalizations for each of the individual arguments. At the next layer we select among those correct formalizations the ones which honor the argument’s dialectic role, i.e. attacking or supporting other arguments as intended. We operate at these two layers in parallel and continuously rate sentences’ formalizations by using, primarily, inferential adequacy criteria. An interpretive, logical theory will thus gradually evolve. This theory is composed of meaning postulates serving as explications for concepts playing a role in the analyzed arguments. Such a recursive, iterative approach to interpretation does justice to the inherent circularity of understanding: the whole is understood compositionally on the basis of its parts, while each part is understood only in the context of the whole. We summarily discuss previous work on exemplary applications of human-in-the-loop computational hermeneutics in metaphysical discourse. We also discuss some of the main challenges involved in fully-automating our approach. By sketching some design ideas and reviewing relevant technologies, we argue for the technological feasibility of a highly-automated computational hermeneutics.

Computational philosophy is the use of mechanized computational techniques to unearth philosophical insights that are either difficult or impossible to find using traditional philosophical methods. Computational metaphysics is computational philosophy with a focus on metaphysics. In this paper, we (a) develop results in modal metaphysics whose discovery was computer assisted, and (b) conclude that these results work not only to the obvious benefit of philosophy but also, less obviously, to the benefit of computer science, since the new computational techniques that led to these results may be more broadly applicable within computer science. The paper includes a description of our background methodology and how it evolved, and a discussion of our new results.

Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects. This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms is simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics. Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics.

We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand’s False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand’s Modus Ponens Elimination. Besides Herbrand’s Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, we carefully investigate Herbrand’s notion of intuitionism in connection with his notion of falsehood in an infinite domain. We sketch Herbrand’s two proofs of the consistency of arithmetic and his notion of a recursive function, and last but not least, present the correct original text of his unification algorithm with a new translation.