The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics

1 Introduction

Without exaggeration Kurt G¨odel's ontological argument for the existence of God [G¨odel, 1970; Scott, 1972] is amongst the most discussed formal proofs in modern literature. A rich body of publications - including very recent ones - present, discuss, assess, criticize, modify and improve G¨odel's original work (see e.g. Sobel [2004] and Oppy [2015] and the references therein). In philosophy lectures at universities the argument is regularly presented as a masterpiece argument in metaphysics. Since 2013, when Benzm¨uller and Woltzenlogel-Paleo [2013a; 2014] first reported their successful initial computer-assisted analysis of G¨odel's proof and Scott's variant, their work has received a media repercussion on a global scale 1 , and numerous bloggers commented

⇤ This work was supported by the German National Research Foundation (DFG) under grants BE 2501/9-2 and BE 2501/11-1.

1 A collection of news articles is available at https://github.com/ FormalTheology/GoedelGod/blob/master/Press/LinksToNews.md

Bruno Woltzenlogel Paleo

Australian National University bruno.wp@gmail.com

on the proof [Fuhrmann, 2016].

The in-depth analysis presented here substantially extends previous computer-assisted studies of G¨odel's ontological argument. Similarly to the related work [Benzm¨uller and Woltzenlogel-Paleo, 2013a; 2014] the analysis has been conducted with automated theorem provers for classical higherorder logic (HOL; cf. [Andrews, 2014] and the references therein), even though G¨odel's proof is actually formulated in higher-order modal logic (HOML; cf. [Muskens, 2006] and the references therein). To bridge between the two logics we utilise and further improve the logic embedding approach [Benzm¨uller and Paulson, 2013; Benzm¨uller and Woltzenlogel-Paleo, 2014], which has already been employed successfully in preceding related work.

The main novel contribution reported in this paper is a detailed analysis (in various modal logics) of the inconsistency of G¨odel's original version of the axioms used in his manuscript [1970]. The extraction, reconstruction and verification of an informal, human intuitive argument has been an open problem since the first detection of this inconsistency by Benzm¨uller and Woltzenlogel-Paleo [2014] with the Leo-II prover. The verified refutation (discussed in §4) displays a surprisingly accessible explanation of the inconsistency, which is philosophically profound and never presented in the literature. The detection of this inconsistency in combination with the work reported here thus demonstrates that artificial intelligence systems - particularly higher-order automated theorem provers - are capable of assisting in the discovery and elucidation of new and philosophically relevant knowledge.

On the technical side, the quest for constructing a compelling refutation, capable of convincing also human nonexperts, led to an improvement of the syntax of the embedding of modal logics in Isabelle/HOL (as discussed in §3.2). With the new syntax, a (nearly) perfect match between the original pen and paper presentations and our encoding in Isabelle/HOL is feasible. A more user-friendly syntax, as reported here, is clearly an important prerequisite for promoting the theorem proving technology employed here to a wider community of philosophers, who are not necessarily experts in automated reasoning or HOL.

Another novel contribution reported here (in §3.1) is the implementation of an alternative embedding for the more effective modal logic S5 U , which is based on a universal accessibility relation. Our experiments have shown that the new embedding is more efficient, as the following two previously open problems can now be solved:

• Automatically proving the final theorem T3 (Necessarily, there exists God), directly from Scott's [1972] (consistent) axioms alone, without relying on the argument's intermediate argumentation steps (i.e., lemmata).
• Automatically verifying, in Isabelle/HOL, the proof of the modal collapse [Sobel, 1987], which is one of the most strongly criticized logical consequences of the argument's axioms.

1.1 RelatedWork

First successful applications of theorem proving technology in metaphysics were reported by Fitelson, Oppenheimer and Zalta [2007; 2011], who coined the term Computational Metaphysics for this new research area and employed the first-order Prover9 [McCune, 2010] in their experiments. Later on, Rushby [2013] used the proof assistant PVS [Owre et al., 1992]. Common to both works is a significant amount of proof-hand-coding work as well as their focus on a nonmodal formalization of St. Anselm's [1078] simpler and older ontological argument. In contrast, the greater complexity of G¨odel's argument requires the formalization and automation of variants of higher-order and modal logics.

2 A Brief History of the Argument

St. Anselm's ontological argument [Anselm, 1078] can be regarded as the ancestor of modern ontological arguments such as G¨odel's. In the millenium between Anselm and G¨odel, many philosophers modified and arguably improved Anselm's argument. Of particular importance to G¨odel was the work of Leibniz [Adams, 1995]. Although G¨odel's notion of positive property is not exactly the same as Leibniz's notion of perfection, G¨odel's manuscript (Fig. 6a) can be considered a translation of Leibniz's presentation of the argument into modern modal logic. G¨odel discussed his manuscript with Scott, who shared a slightly di↵erent version with a larger public. Scott's version of the axioms and definitions, formalized in Isabelle, is shown in Fig. 1. The main di↵erence to G¨odel's version is an extra conjunct in the definition of essence (ess). G¨odel's di↵erent definition of essence can be seen either in his manuscript (Fig. 6a) or, in more modern notation, in the Isabelle formalization shown in Fig. 5. For Scott, an essential property of an individual must be possessed by him/her. For G¨odel, this is not required.

G¨odel's omission has been considered inessential and merely an oversight by many. For instance, Hazen [1998, p.365] states that "G¨odel left this clause out [. . . ] but this appears to have been an oversight". For more than four decades, its serious consequences remained unnoticed, despite numerous analysis and criticisms of the argument. Especially since the discovery by Sobel [1987] that modal collapse (MC) 2 is entailed by G¨odel's (or also Scott's) axioms, several variants have been proposed [Anderson, 1990; Anderson and Gettings, 1996; H´ajek, 1996; 2001; H´ajek, 2002; Bjørdal, 1999] attempting to avoid the modal collapse. Many of these variants omit the crucial conjunct in the definition of essence as well. 3 Opponents of the argument (e.g. Oppy [1996, p.226-227; 2000, p.364; 2008, p.1068]) have also proposed parodies and other criticisms, referring to variants where the conjunct is omitted.

2 The modal collapse, φ ! ⇤φ, states that contingent truth implies necessary truth; it can be interpreted as everything is predetermined or even there is no free will.

However, as explained here, the extra conjunct is in fact crucial. Without it, G¨odel's original axioms are inconsistent. With it, Scott's axioms are consistent (cf. Fig. 1 where the model finder Nitpick [Blanchette and Nipkow, 2010] confirms consistency). 4

3 Automating HOML in HOL

Logic textbooks commonly utilize higher-order logic in an informal/semi-formal way as a meta-language to introduce the syntax and the semantics of object logics of interest, in which reasoning problems in concrete application domains can be modeled and solved with pen and paper. In fact, this approach can also be followed on the computer (using HOL as a formal meta-language) for even very challenging object logics (such as HOML) to enable interactive and automated theorem proving with existing theorem provers for HOL.

3 As these variants also change other axioms, on which the inconsistency of G¨odel's axioms depends, it is not necessarily the case that these variants are also inconsistent; they must be analyzed separately.

4 In personal communication, Dana Scott confirmed that he was unaware at the time that G¨odel's axioms were inconsistent.

For a computational analysis of G¨odel's ontological argument, the embedding of HOMLs such as K, KB and S5 with various domain conditions (possibilist and actualist quantification) is required. This idea has been successfully employed in related work [Benzm¨uller and Woltzenlogel-Paleo, 2014]. The embedding of HOML is in fact straightforward. Formulas in HOML are lifted, i.e., converted into predicates over worlds, which are themselves explicitly represented as terms. The logical constants of HOML are translated to HOL terms in such a way that, for instance, ⇤' and ^' (relative to a current world wo) are mapped, respectively, to the HOL formulas 8w.(rw0w)!('w) and 9w.(rw0w) ^ ('w). This form of embedding is precisely the well-known standard translation [Ohlbach, 1991], which is here intra-logically realized - and extended for quantifiers - in HOL by stating a set of equations defining the logical constants (Fig. 2). The resulting object logic is the HOML K with rigid terms and constant domains (possibilist quantifiers). Other logics (e.g. KB, S5) are embedded by adding axioms that restrict the accessibility relation r. Varying domains and actualist quantifiers can be simulated by using an existence predicate to guard the quantifiers. The embedding approach is, therefore, very flexible.

3.1 Improved Embedding

The modal logic S5 requires that the accessibility relation be reflexive, symmetric and transitive. The usual approach to embed S5 would be to use the standard translation for K described above and to state that r is an equivalence relation, e.g., by postulating the following axioms:

• Reflexivity: 8x.(r x x)
• Symmetry: 8x.8y.(r x y) ! (r y x)
• Transitivity: 8x.8y.8z.(r x y) ^ (r y z) ! (r x z)

Instead, we consider here an alternative description, that we call S5 U , based on the following condition on r:

• Universality: 8x.8y.(r x y)

It is important to note that ✏S5 ' i↵ ✏S5 U ' [Blackburn et al., 2001], and therefore S5 and S5 U are traditionally considered to be two di↵erent descriptions of the same modal logic. Nevertheless, S5 and S5 U di↵er in the shapes of frames they admit: S5 U only admits complete 5 frames, whereas S5 admits non-complete frames as long as all their components are complete. In other words, in S5 U we face one single equivalence class of possible worlds, while in S5 we may face several disconnected equivalence classes. In fact, for this reason, S5 U is considered as metaphysically more appropriate by some philosophers; cf. [Williamson, 2013, p. 127].

Furthermore, for S5 U an improved embedding is possible. Universality implies that the guarding predicates in the definitions of ⇤ and ^ always hold. Therefore, they can be omitted and the accessibility relation can be dispensed altogether. The modal operators can then be defined merely as:

⇤' ⌘ λw.8v.'(v) and ^' ⌘ λw.9v.'(v)

The new embedding of S5 U in Isabelle/HOL is shown in Fig. 2. With this improved embedding, the final theorem T3 (Necessarily, there exists God) can be derived from Scott's consistent version of the axioms fully automatically. The fully automatic proof has been generated (in about 2.5 seconds) by the theorem prover Leo-II [Benzm¨uller et al., 2015] and subsequently verified in the proof assistant Isabelle/HOL [Nipkow et al., 2002], as shown in Fig. 1. The collaboration between the two systems has been orchestrated by Isabelle's Sledgehammer tool [Blanchette et al., 2013].

With the embedding used by Benzm¨uller and Woltzenlogel-Paleo [2014], the provers still had to be given the intermediate theorem T2 and the corollary C in order to manage to prove T3.

Another evidence that the new embedding provides a significant performance boost is the successful automatic verification in Isabelle/HOL (with its automatic tactic Meson) of the modal collapse [Sobel, 1987], which is one of the most strongly criticized 'side-e↵ects' of G¨odel's and Scott's variants of the proof. In previous work [2014] the modal collapse has been proven by the higher-order provers Satallax [Brown, 2012] and Leo-II, but a fully automatic verification in the highly trusted Isabelle/HOL system still failed [Benzm¨uller and Woltzenlogel-Paleo, 2013b]. The success with the new embedding can be seen in Fig. 1.

5 A graph is complete i↵ there is a directed edge connecting every ordered pair of vertices.

Figure 3: Definition of Essence using Old Syntax

3.2 Improved Syntax in Isabelle

Wider adoption of HOL theorem proving technology for reasoning about and within embedded object logics, especially among non-expert users, is still hindered by the gap between the syntax used by people, when they write logical formulas with pen and paper, and the syntax used by HOL theorem provers. Even when the syntax of the underlying higher-order system is elegant (as is the case in Isabelle/HOL), the embedding of HOML into HOL may easily expose details of HOL that may be uncommon to the user, disturbing his/her experience while using the system. To illustrate this point, Fig. 3 shows how the definition of essence looked like in previous work [Benzm¨uller and Woltzenlogel-Paleo, 2013b], where advanced syntax-sugaring features were not used. It looks notably higher-order, and its style di↵ers significantly from the common style seen in works on modal logics and the ontological argument. The following specific issues can be enumerated:

1. λ-abstractions, which are typically a HOL feature, appear explicitly in places where they did not need to in a pure HOML formulation (cf. G¨odel's manuscript, Fig. 6a).
2. Quantifiers appear as higher-order defined constants, and not as binders. This forces the user to read (and write) formulas of the form 8(λx.A(x)) instead of the more common 8x.A(x).
3. The lifted modal connectives are represented by prefixing the letter "m" (e.g. m^ and m!). The prefix disturbs the user, as it constantly reminds him/her that there is something unusual about the modal connectives.
4. Higher-order parenthesis conventions for the application of a predicate to a termare used. Instead of reading (y), as he/she would expect, he/she has to read ( y). Outside niche areas in computer science, the former syntax is more widely known than the latter.

In the embedding presented here, in Fig. 2, advanced syntax-sugaring e↵ects provided by Isabelle were used to prevent issues as those enumerated above. The possibility to define boldface connectives allows us to drop the prefix; "binder" annotations enable modal quantifiers to be used in the standard binding way and reduce the need for explicit lambda abstractions; and a careful choice of priorities for infix connectives gives the parenthesis conventions that are more familiar to the user. As desired, the definition of essence in Fig. 1 is undeniably more immediately recognizable and comprehensible than the definition in Fig. 3. The embedding technique is now completely transparent to the user.

The syntax improvements described here render the computer-assisted analysis of ontological arguments accessible to a wider audience and ease the adoption of logic-based artificial intelligence tools by philosophers interested in topics where modal logic reasoning is required.

4 Intuitive Inconsistency Argument

In the typical workflow during an attempt to prove a conjecture with a theorem prover, it is customary to check the consistency of the axioms first. For if the axioms are inconsistent, anything (including the conjecture) would be trivially derivable in classical logic (ex falso quodlibet). Surprisingly, when this routine check was performed on G¨odel's axioms [Benzm¨uller andWoltzenlogel-Paleo, 2014], the LeoII prover claimed that the axioms were inconsistent. Unfortunately, the refutation generated by Leo-II was barely human-readable. The text file was 153 lines 6 long and used machine-oriented calculus (higher-order resolution [Sultana and Benzm¨uller, 2013]) and syntax (TPTP THF [Sutcli↵e and Benzm¨uller, 2010]). Part of the file is displayed in Fig. 4.

Although Leo-II's resolution refutation is not easy to read for humans, it did contain relevant hints to the importance of the empty property λx.? (also denoted ;, as in HOL it is customary to think of unary predicates as sets). Note that the terms for the empty property 7 (λx.?) and for the property of self-di↵erence (λx.x , x) have identical denotations in a logic setting with full functional and Boolean extensionality as given here. Nevertheless, some philosophers 8 may actually prefer the use of self-di↵erence over the empty property in the analysis below. However, for the proof to go through it is irrelevant which notion we use and the reader may simply replace the empty property by self-di↵erence.

4.1 Informal Argument

Based on the hints found in Leo-II's refutation, we conceived the following informal explanation for the inconsistency of G¨odel's axioms:

1. From G¨odel's definition of essence (φ ess x $ 8 ( (x)!⇤8y(φ(y)! (y)))) it follows that the empty property (or self-di↵erence) is an essence of every individual (Empty Essence Lemma):

1. From theoremT1 (Positive properties are possibly exemplified: 8φ[P(φ)!^9xφ(x)]) and axiom A5 ("necessary existence" is a positive property: P(NE) ), it follows that NE is possibly exemplified:

1. Expanding the definition of "necessary existence" (NE(x) ⌘ 8φ[φ ess x!⇤9yφ(y)]), the following is obtained:

1. The sentence above holds for all ' and thus, in particular, for the empty property (or self-di↵erence):

6 Long lines with an average of 184 characters per line.

7 An additional lambda abstraction occurs in the empty property in Leo-II's proof (and also in the reconstruction in Isabelle) because the embedding approach lifts the boolean type o to ◆!o.

8 Private communication with Andr´e Fuhrmann.

Figure 4: Lines 115-120 of Leo-II's refutation. Primitive substitutions (e.g. with the empty property) are highlighted. In the red part (see ), property variable SV8 has been instantiated with the λSV16µ.λSV17◆.?, i.e., the (lifted) empty property.

1. By the Empty Essence Lemma, the antecedent of the implication above is valid. Therefore, the sentence above entails:
2. By definition of ;:

1. As the existential quantifier is binding no variable within its scope, the sentence is equi-valid with:

^⇤?

1. To see that the sentence above is contradictory, we may reason semantically, thinking of possible worlds. If w0 is the arbitrary current world, the ^ operator forces the existence of a world w accessible from w0 such that ⇤? is true in w. But ⇤? can only be true in w, if there is no world w 0 accessible from w. In logics with a reflexive or symmetric accessibility relation (e.g. KB), it is easy to see that there must be a world w 0 accessible from w: either w 0 itself, in case of a reflexive relation, or w0, in case of a symmetric relation. In fact, even in K, with no accessibility condition, there must be a world w 0 accessible from w. The reason is that ^⇤? should be valid (true in all worlds). Therefore, it is true in w as well, where the existence of an accessible world w 0 is forced by the ^ operator. As a model for ^⇤? (which is a consequence of G¨odel's axioms) cannot be built, G¨odel's axioms are inconsistent.

Interestingly, the refutation automatically generated by Leo-II uses a symmetric accessibility relation, and thus requires the modal logic KB. The informal, human-constructed refutation described above, on the other hand, requires only the weaker modal logic K. In our experiments Leo-II (like all other HOL provers) was still too weak to automatically prove the inconsistency already in logic K. Hence, this remains an open problem for automated theorem provers.

4.2 Argument Reconstruction in Isabelle

To verify the correctness of the informal argument explained above, it was reconstructed in Isabelle/HOL, using Metis 9 to automate the inessential parts (cf. Fig. 5). The essential use of the Empty Essence Lemma, on the other hand, is explicitly stated, to ensure that Isabelle is reconstructing the same argument. In fact, without the help of this lemma, Metis is still not strong enough to refute G¨odel's axioms.

9 Metis, unlike external provers such as Leo-II or Satallax, constructs proofs in Isabelle's highly trusted kernel calculus.

4.3 Mapping the Inconsistency to G¨odel

The inconsistency verified in Fig. 5 follows from the definition of essence (ess), the definition of necessary existence (NE), the axioms A1a and A2 (which entail theorem T1), and axiomA5. It remains to show that these ingredients are actually present in G¨odel's manuscript in Fig. 6a.

This can be easily seen: Axiom A1a in Fig. 5 is implied by Axiom Ax2 and the highlighted footnote remark in Fig. 6a. Axioms A2 and A5 in Fig. 5 correspond to Ax4 and Ax3 in

(a) G¨odel's manuscript, with mutually inconsistent axioms and definitions highlighted (with permission from the Kurt G¨odel Papers, Shelby White and Leon Levy Archives Center, Princeton, NJ, USA, on deposit at Princeton University)

• (b) Inconsistency in HOML S5 U

Figure 6: The inconsistency in G¨odel's manuscript has been detected and verified by HOL ATPs

Fig. 6a. The definitions of essence and necessary existence are easy to identify. Therefore, the verified inconsistency from Fig. 5 does apply to G¨odel's original manuscript.

4.4 Inconsistency of G¨odel's Axioms in S5 U

Isabelle/HOL's Sledgehammer tool, which orchestrates calls to external provers such as Leo-II, still fails to detect the inconsistency of G¨odel's axioms in the standard embedding of S5, while a direct modeling of the problem in TPTP THF syntax in combination with a direct call of Leo-II succeeded. In other words, without independent experiments with no mediation through Sledgehammer, the inconsistency would not have been detected.

On the other hand (and further confirming the claims from §3.1), the reconstruction in Isabelle/HOL with the improved embedding for S5 U was more efficient: the inconsistency could be detected by Leo-II also when called via Sledgehammer. Moreover, the result could subsequently be verified with Metis even without the Empty Essence Lemma (cf. Fig. 6b).

5 Conclusion

The axioms and definitions in G¨odel's manuscript are inconsistent; this was detected automatically by the prover Leo-II. Here we presented a rational reconstruction and verification of the inconsistency argument in Isabelle/HOL. This argument is valid in all normal HOMLs including base logic K.

We have also presented several technical improvements regarding the semantic embedding approach. In particular, we have achieved a nearly perfect match between pen and paper presentations in HOML and the syntax in Isabelle/HOL. As a result, the embedding of HOML in HOL is now fully transparent, more user-friendly and ready for wider adoption.

On the other hand, there is still room for many pragmatical improvements in Isabelle; just one example: in default setting, Sledgehammer does not immediately inform the user when a proof has been found and instead silently first executes a series of time-consuming proof analysis processes (e.g. its dependency minimization), before it eventually reports success. For G¨odel's theorem T3 (Necessarily, there exists God), for example, this phase of silence takes several minutes - during which the user might actually give up on the proof attempt - even though Leo-II already reported success to Sledgehammer after 2.5 seconds.

More importantly, our work reveals a challenge for automated reasoning: the (so far partially manual) extraction of an informal argument from a formal proof. Without accompanying human-understandable explanations, the proofs generated by provers such as Leo-II or Metis, will presumably be only of limited value for philosophers, for whom intuitive arguments remain crucial for the acceptance of novel results.

Another open problem that we solved in this paper is a fully automatic proof of T3 directly from Scott's axioms. Again, this proof was contributed by Leo-II. This has become possible only after we provided a more efficient embedding for HOML S5 U (instead of S5) in HOL.

Both the automated detection of the inconsistency in G¨odel's axioms and the fully automatic proof of T3 from Scott's axioms demonstrate the potential of our AI technology for philosophy: this technology is, in its current state of development, already capable of contributing novel results to metaphysics and to conduct reasoning steps at granularitylevels beyond common human capabilities.

Acknowledgments: We thank Chad Brown, who contributed to the rational reconstruction of the inconsistency argument.