Christoph Benzmüller is Full Professor for AI Systems Engineering at the Otto‐Friedrich‐University Bamberg, Bamberg, Germany; e‐mail: christoph‐benzmueller@uni‐bamberg.de (or c.benzmueller@gmail.com).

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.

The field of AI has already experienced various winter and summer periods in its comparatively young history. The current “heat wave” seems to be stronger and more sustained than previous summer periods, as significant progress has been made in the last two decades, especially in the area of ^{1}

The vision of

AI is a science of computer technologies developed to achieve and explain

Excellent progress in the field of AI has been made primarily at level (i) and to some extent at level (ii); this progress at both levels has been enabled by both subsymbolic and symbolic techniques, although the emphasis at present, especially at level (i), seems to be more on the former. Progress at level (iii), in my view, clearly requires symbolic modeling and reasoning skills in an intelligent entity; in particular, the exploration and subsequent evaluation of an abstract theory, say in mathematics, traditional natural sciences, or metaphysics, inevitably involves mastering a

Moreover, in mathematics and metaphysics in particular, abstract theories are not seldom explored using

The computer‐supported experiment on the ontological argument reported in the next section has thus a twofold function in this article. First, it serves as one, small piece of evidence for recent advances in the field of knowledge representation and reasoning (KR&R), that is, symbolic AI, which has led to new insights that are relevant for philosophy and rational theology. Second, it provides evidence for the claim that the creation, use, and manipulation of explicit symbolic representations is central to certain scientific discovery processes. In other words, a strong AI lacking explicit KR&R skills appears essentially inconceivable to me.

What is the simplified ontological argument, resp. simplified ontological theory, the computer helped to explore? I switch from “argument” to “theory” here, since not only the pure argument is of interest for our investigation, but also some further implications arising from the axioms and definitions of the argument (cf. the modal collapse [MC] below).

This new theory resulted from a series of experiments in which Scott's (

The notion of positive properties is taken by both Gödel and Scott as the single primitive notion, based on which the concept of a Godlike entity is then defined by (definition D1) “A Godlike entity possesses all positive properties.” Axiom A1 states that “Either a property or its negation is positive, but not both,” and Axiom A2 expresses “A property is positive if it is necessarily entailed by a positive property”; property entailment is defined here using material implication. Axiom A3, in Scott's variant,^{2}

The above axioms and definitions of Scott's theory variant were in a first round of experiments formalized in a higher order modal logic S5,^{3}

The conducted experiments quickly confirmed the validity of each of the following argument steps; thereby the theorem provers automatically identified the minimal dependencies as shown in brackets; from these assumptions the statements follow:

T1: “Positive properties are possibly exemplified” (from A1, A2).

C: “Possibly there exists a Godlike being” (from A3, T1).

T2: “Being Godlike is an essence of any Godlike being” (from A1, A4, D1, D2).

T3: “Necessarily, there exists a Godlike being” (from A5, B, D1, D3, C, T2).

T4: “There exists a Godlike being” (from B, T3, C).

Subsequently, further implied theorems were explored, including:

MC: “What holds, holds necessarily (no contingent truths)” (from A1, A4, B, D1, T3).

C1: “Self‐difference (or empty property) is not a positive property” (from A1, A2)

C2: “A property is positive if it is entailed by a positive property” (from A1, D1, T4)

U: “Positive properties form a (modal) ultrafilter” (from A1, A2, B, D1, T3, MC)

C1 and C2 are two of the filter/ultrafilter properties that were tested in step U of the experiments; the reason they are additionally listed here, resp. singled out, will become clear below.^{4}

All the above argument steps were verified by Benzmüller and Woltzenlogel Paleo (

These successful experiments were then later taken as a starting point by Fuenmayor and Benzmüller (

The ultrafilter perspective was then also the trigger for the investigation of the strongly simplified variant presented in Figure

The new simplified theory starts out with unmodified definition of a Godlike entity as an entity that possess all positive properties, in which the notion of “positive property” is the only primitive concept that is further constrained by the following three axioms:

C1: “Self‐difference, or, alternatively, the empty property, is not a positive property.”

C2: “A property is positive if it is entailed by a positive property.”

A3: “Being Godlike is a positive property.”

The assumed logic for the moment is a modal logic K. It follows:

L1: “The existence of a non‐exemplified positive property implies that self‐difference (resp. the empty property) is positive” (from A2', since such a nonexemplified positive property would entail self‐difference, where entails is defined as: for all , () implies ()).

L2: “A non‐exemplified positive property does not exist” (from A1' and the contrapositive of L1).

T1’: “Positive properties are exemplified” (a simple reformulation of L2).

T4: “There exists a Godlike being” (follows from A3 and T1').

T3: “Necessarily, there exists a Godlike being” (from T4, by necessitation).

Interestingly, the possibility of the existence of a God‐like being cannot be easily proved in the basic modal logic K, and Nitpick reports a countermodel. However, this circumstance can be countered simply by switching to modal logic KT, that is, by adding the modal axiom T (the T axiom states, “What necessarily holds, holds” or, alternatively, “What holds, is possible”). Moreover, in modal logic KT also the following alternative proof variant was automatically confirmed by the theorem provers integrated with the Isabelle/HOL proof assistant; this variant is close to the variant by Scott as shown at the beginning:

T1: “Positive properties are possibly exemplified” (from A1', A2', T).

C: “Possibly there exists a Godlike being” (from A3, T1).

T2': “The possible existence of a Godlike being implies its necessary existence” (from A3, A1', A2').

T3: “Necessarily, there exists a Godlike being” (from T2', C).

T4: “There exists a Godlike being” (from T3, T).

Future work includes the computational study of the relationship of the above human‐explored simplified variants of the modal ontological argument to other variants of the argument that are still less known in the literature, such as Gustaffson (

As the above experiments show, modern symbolic AI technology can thus make a fruitful contribution to the rigorous evaluation of existing arguments and theories in metaphysics and rational theology, and even support the exploration of new, simplified theories. Thanks to the LogiKEy methodology, even the object logics in which the domain theories of interest are modeled and encoded become negotiable (i.e., subject to modification, extension, or replacement) and thus objects of study in the computer. Currently, however, a collaboration triangle is still required, involving a domain expert (e.g., philosopher or theologian), an AI expert/logician (who is proficient in the automated and interactive reasoners and the LogiKEy methodology), and the AI reasoners. In the future, the AI expert/logician should ideally become less and less relevant as AI reasoners continue to improve both proof automation and intuitive user interaction. Assuming a strong AI vision, another interesting question arises. Namely, whether an AI reasoner initialized with an appropriately represented object logic, a domain theory, and a proof argument as a starting point can eventually perform a creative process as the one described in the section “A Computationally Explored Simplified Variant of the Ontological Argument,” but completely autonomously.

After hours of theorizing, in which the AI continuously manipulates and (re)assesses these representing objects, it would then, for example, inform humans of the most interesting simplified or new alternative theories (and their assumed object logics) that it has explored along the way, or it would return interesting countermodels that it has found. In the spirit of our initial discussion, such a vision could then even be seen as a shift from metaphysics and rational theology toward an experimental, natural science in which representing objects of these domains are physically manipulated and assessed in the computer. This is, of course, a controversial vision that in itself deserves further analysis.

In summary, symbolic AI can do much for metaphysics and rational theology. Conversely, metaphysics and rational theology are of particular interest to AI research, especially because of the prominent role that thought experiments and abstract arguments play in these disciplines in combination with the typical absence of “real world” data. These disciplines therefore particularly emphasize the need for explicit symbolic representations and theorizing with little or no data.

Open Access funding enabled and organized by Projekt DEAL.

Since its very beginnings, the field of AI has differentiated between the

In Gödel's scriptum we find the more complex (third‐order) axiom: “The conjunction of any collection of positive properties is positive”; let's call this A3*. Using D1, it can be shown that A3 is a consequence of A3* (in modal logic K) and, moreover, A3 suffices for establishing the intended results. Scott thus found it reasonable to replace A3* by the much simpler axiom A3.

And additionally a logic S5U was used in the experiments by Benzmüller and Woltzenlogel Paleo (

An ultrafilter U (on sets) is a filter satisfying an additional maximality criterion (for each property