Artificial Intelligence (AI): Symbolic versus Subsymbolic

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 subsymbolic AI. ¹ Data‐driven machine learning methods, particularly deep learning, have been hyped in the media, and industry is desperately seeking and hiring experts, since AI is widely considered the steam engine of the twenty‐first century. These success stories have even led to the term AI being largely reduced to subsymbolic AI in the public perception today. At the same time, symbolic AI is now often referred to as good old fashioned AI (GOFAI), which is clearly a misleading term, as both symbolic and subsymbolic AI techniques have been explored as relevant from the beginning, particularly with respect to visions of strong AI. And as will be discussed below, there are success stories to report in the area of symbolic AI as well, although not at the level of subsymbolic AI, which currently promises to be a very robust and viable choice for many low‐hanging fruit applications in industry.

The vision of strong AI, that is, AI that surpasses human capabilities in all or almost all domains, requires, in my view, the hybridization of techniques from both sides (or a convincing explanation of why symbolic reasoning techniques should suddenly and readily evolve from data‐driven subsymbolic techniques). It is thus in fact the area of hybrid AI where the next “big (intellectual) thing” is to expected. To better understand my viewpoint and to see why I continue to insist on the relevance of symbolic AI, it appears useful that I briefly present my personal working definition of the term AI:

AI is a science of computer technologies developed to achieve and explain intelligent behavior in machines. By intelligent I refer here to a collection of abilities that enable an entity to (i) solve or learn how to solve certain (difficult) domain specific problems, (ii) master the known and the unknown, i.e., to act successfully in known, unknown, and dynamic environments (which requires perception, planning, agency, etc.), (iii) think rationally, avoid contradictions, and explore abstract theories, (iv) self‐reflect, recognize self‐contradictions, and reconcile one's reasoning with higher‐level goals and norms, and (v) interact socially with other entities and reconcile one's goals and norms with those of a community (for a greater good).

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 symbolic representation language. Bibel (2022) has therefore introduced the term “representing objects” to refer to the elements of this language, and he argues that with the invention of the computer a “new natural science” has emerged, capable of theorizing about representing objects that are enabled by AI as scientific discipline (including, in particular, symbolic AI) and which is way more than just a set a of, for example, machine learning tools.

Moreover, in mathematics and metaphysics in particular, abstract theories are not seldom explored using very little or no experimental data. An example is the ontological argument for the existence of God, since it is based entirely on concepts and definitions explored by abstract thought. Among the several kinds of ontological arguments, the one formulated in modern modal logic by Kurt Gödel and subsequently modified by Dana Scott and others has been the focus of some of my own work with colleagues over the past decade. This research has been conducted with fruitful human‐machine interaction by utilizing symbolic representation and communication techniques, and it has now led to the exploration of a highly simplified theory, which can, in turn, further inform human insight into the ontological argument. While so far only parts of the exploration process have been fully automated by symbolic AI reasoners (automated theorem provers and model finders), there are indications that the pendulum here may swing more strongly toward such symbolic AI reasoners and increased automation in the future (especially when future hybrid AI systems will be used). In purely subsymbolic AI systems, lacking any symbolic representation means, neither abstract theory exploration nor subsequent theory evaluation or adequate communication with humans seems sufficiently well supported to enable fruitful theory exploration. In other words, subsymbolic AI skills will hardly be sufficient to automate abstract theory exploration processes in intelligent agents, since such processes seem inherently dependent on formal (symbolic) language skills.

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.

A Computationally Explored Simplified Variant of the Ontological Argument

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 (1972) variant of Gödel's (1970) theory has been taken as the starting point of investigation. In Figure 1, I briefly recap Scott's theory before I present the new simplified theory.

Figure   1

Figure   1 Experiments on Scott's Variant of Gödel's Modal Ontological Argument. [Colour figure can be viewed at ]

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, ² simply postulates that “Being Godlike is a positive property,” and Axiom A4 that “Any positive property is necessarily positive.” Axiom A5 finally states that “Necessary existence is a positive property,” where “x necessarily exists if all of its essential properties are necessarily exemplified” (definition D3); definition D3 in turn uses the term “essential properties,” resp. “essence,” which is defined by “A property φ is an essence of an entity x if, and only if, (i) φ holds for x and (ii) φ necessarily entails every property ψ of x” (definition D2). The clause (i) in D2 is omitted in Gödel's (1970) variant and was added by Scott (because he found it an intuitive and natural to do so).

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, ³ whereas the logic S5 was itself introduced, utilizing the logic‐pluralistic KR&R methodology termed LogiKEy (Benzmüller et al. 2020), as a theory of classical higher‐order logic (HOL). Due to this nested theory construction, off‐the‐shelf interactive and automated theorem provers for HOL became readily applicable to support an in‐depth formal assessment of Scott's ontological theory with computers.

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. ⁴

All the above argument steps were verified by Benzmüller and Woltzenlogel Paleo (2014, 2015, 2016a) with the Leo automated theorem provers (Benzmüller et al. 2015; Steen and Benzmüller 2021) for HOL and later also with the interactive proof assistants Isabelle/HOL (Nipkow et al. 2002) and Coq (Bertot and Casteran 2004). In addition, the Nitpick model finder (Blanchette and Nipkow 2010) for HOL was used to automatically confirm the consistency of the theory; it provided a simple model. However, when clause (i) in definition D2 was omitted in the experiments, no such model was found anymore, suggesting an attempt to infer falsity from the axioms of the theory. The theorem prover Leo‐II actually succeeded in this and computed a resolution‐style proof, which, with some delay, was analyzed and converted by Benzmüller and Woltzenlogel Paleo (2016a, 2016b) into a human‐readable intuitive proof argument. This first round of experiments with the modal variants of Gödel and Scott's ontological argument was thus very successful. The first variant was shown to be inconsistent and the second variant valid, and for this the theorem provers needed only the modal logic KB and not the modal logic S5, as it is had been controversially discussed in this context.

These successful experiments were then later taken as a starting point by Fuenmayor and Benzmüller (2017) and Benzmüller and Fuenmayor (1990) not only for the verification of Fitting's (2002) modal variant but also for an extended, comparative study of Fitting's with the modal variants of Anderson (1990), resp. Anderson and Gettings (1996). In these experiments, it was shown that both Fitting's and Anderson's variants were also both valid and that they indeed, as intended by their authors, avoid the controversial MC. While both variants are seemingly different, they are nevertheless related when comparing these variants through “ultrafilter lenses”; they apply related relaxations regarding the concrete ultrafilter properties that must be satisfied by the set of positive properties (more precisely, the set of modally rigidified positive properties).

The ultrafilter perspective was then also the trigger for the investigation of the strongly simplified variant presented in Figure 2. Thereby, the two special ultrafilter properties C1 and C2 from above proved to be especially interesting, because, as the computer automatically confirmed, the existence (resp. necessary existence) of a God‐like entity can already be derived very easily in the basic modal logic K (resp. in the modal logic KT) from these two corollaries of Scott's theory in combination with the Axiom A3.

Figure   2

Figure   2 Simplified Variant of Gödel's Ontological Argument; Explored in a Human‐Machine Interaction. [Colour figure can be viewed at ]

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 (2020), Gödel's variant #2 discussed by Kanckos and Lethen (2021), and the proposals by Świetorzecka and Łyczak (2020) and Christian (1989).

Metaphysics and Rational Theology as an Experimental Science?

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.

Acknowledgment

Open Access funding enabled and organized by Projekt DEAL.