93

ECAI 2014
T. Schaub et al. (Eds.)© 2014 The Authors and IOS Press.
This article is published online with Open Access by IOS Press and distributed under the termsof the Creative Commons Attribution Non-Commercial License.
doi:10.3233/978-1-61499-419-0-93

Automating Gödel’s Ontological Proof of God’s Existencewith Higher-order Automated Theorem Provers
Christoph Benzmüller1 and Bruno Woltzenlogel Paleo2
Abstract. Kurt Gödel’s ontological argument for God’s existence
has been formalized and automated on a computer with higher-order
automated theorem provers. From Gödel’s premises, the computer
proved: necessarily, there exists God. On the other hand, the theorem
provers have also confirmed prominent criticism on Gödel’s ontological argument, and they found some new results about it.
The background theory of the work presented here oﬀers a novel
perspective towards a computational theoretical philosophy.

1 INTRODUCTION
Kurt Gödel proposed an argumentation formalism to prove the existence of God [23, 30]. Attempts to prove the existence (or nonexistence) of God by means of abstract, ontological arguments are
an old tradition in western philosophy. Before Gödel, several prominent philosophers, including St. Anselm of Canterbury, Descartes
and Leibniz, have presented similar arguments. Moreover, there is
an impressive body of recent and ongoing work (cf. [31, 19, 18] andthe references therein). Ontological arguments, for or against the existence of God, illustrate well an essential aspect of metaphysics:
some (necessary) facts for our existing world are deduced by purely
a priori, analytical means from some abstract definitions and axioms.
What motivated Gödel as a logician was the question, whether it
is possible to deduce the existence of God from a small number offoundational (but debatable) axioms and definitions, with a mathematically precise, formal argumentation chain in a well defined logic.
In theoretical philosophy, formal logical confrontations with suchontological arguments had been so far (mainly) limited to paper andpen. Up to now, the use of computers was prevented, because thelogics of the available theorem proving systems were not expressive
enough to formalize the abstract concepts adequately. Gödel’s proof
uses, for example, a complex higher-order modal logic (HOML)
to handle concepts such as possibility and necessity and to support
quantification over individuals and properties.
Current works [10, 9] of the first author and Paulson illustrate thatmany expressive logics, including quantified (multi-)modal logics,
can be embedded into the classical higher-order logic (HOL), which
can thus be seen as a universal logic [6]. For this universal logic,
eﬃcient automated theorem provers have been developed in recent
years, and these systems were now employed in our work.
Gödel defines God (see Fig. 1) as a being who possesses all positive properties. He does not extensively discuss what positive properties are, but instead he states a few reasonable (but debatable) ax1 Freie Universität Berlin, Germany, email: c.benzmueller@fu-berlin.de; thisauthor has been supported by the German National Research Foundation(DFG) under grants BE 2501/9-1 and BE 2501/11-1.
2 Technical University Vienna, Austria, email: bruno@logic.at

A1 Either a property or its negation is positive, but not both:∀φ[P(¬φ) ≡ ¬P(φ)]
A2 A property necessarily implied by a positive property is positive:∀φ∀ψ[(P(φ) ∧ !∀x[φ(x) ⊃ ψ(x)]) ⊃ P(ψ)]
T1 Positive properties are possibly exemplified:∀φ[P(φ) ⊃ !∃xφ(x)]D1 A God-like being possesses all positive properties:
G(x) ≡ ∀φ[P(φ) ⊃ φ(x)]A3 The property of being God-like is positive:
P(G)C Possibly, God exists:!∃xG(x)
A4 Positive properties are necessarily positive:∀φ[P(φ) ⊃ ! P(φ)]
D2 An essence of an individual is a property possessed by it andnecessarily implying any of its properties:
φ ess. x ≡ φ(x) ∧ ∀ψ(ψ(x) ⊃ !∀y(φ(y) ⊃ ψ(y)))
T2 Being God-like is an essence of any God-like being:∀x[G(x) ⊃ G ess. x]
D3 Necessary existence of an individ. is the necessary exemplification of all its essences: NE(x) ≡ ∀φ[φ ess. x ⊃ !∃yφ(y)]A5 Necessary existence is a positive property:
P(NE)T3 Necessarily, God exists:!∃xG(x)Figure 1.

Scott’s version of Gödel’s ontological argument [30].

ioms that they should satisfy. Various slightly diﬀerent versions ofaxioms and definitions have been considered by Gödel and by several
philosophers who commented on his proof (cf. [31, 3, 2, 19, 1, 18]).
The overall idea of Gödel’s proof is in the tradition of Anselm’s
argument, who defined God as some entity of which nothing greater
can be conceived. Anselm argued that existence in the actual world
would make such an assumed being even greater; hence, by definition
God must exist. Gödel’s ontological argument is clearly related tothis reasoning pattern. However, it also tries to fix some fundamental
weaknesses in Anselm’s work. For example, Gödel explicitly provesthat God’s existence is possible, which has been a basic assumptionof Anselm. Because of this, Anselm’s argument has been criticized asincomplete by Leibniz. Leibniz instead claimed that the assumption
should be derivable from the definition of God as a perfect being andfrom the notion of perfection. Gödel’s proof addresses this critique,and it also addresses the critique of others, including Kant’s objectionthat existence should not be treated as a predicate. On the other hand,Gödel’s work still leaves room for criticism, in particular, his axioms
are so strong that they imply modal collapse, that is, a situation wherecontingent truths and necessary truths coincide. More information on
the philosophical debate on Gödel’s proof is provided in [31].

94

C. Benzmüller and B. Woltzenlogel Paleo / Automating Gödel’s Ontological Proof of God’s Existence with HOL-ATPs

We have analyzed Dana Scott’s version of Gödel’s proof [30](cf. Fig. 1) for the first-time with an unprecedented degree of detail and formality with the help of higher-order automated theorem
provers (HOL-ATPs).3 The following has been done (and in this order): (i) a detailed natural deduction proof; (ii) a formalization in
TPTP THF syntax [33]; (iii) an automatic verification of the consistency of the axioms and definitions with Nitpick [16]; (iv) an automatic demonstration of the theorems with the provers LEO-II [11]and Satallax [17]; (v) a step-by-step formalization using the Coq
proof assistant [15]; (vi) a formalization using the Isabelle proof assistant [26], where the theorems (and some additional lemmata) havebeen automated with the Isabelle tools Sledgehammer and Metis.
Subsequently, we have studied additional consequences of Gödel’s
axioms, including modal collapse and monotheism, and we have investigated variations of the proof, for example, by switching fromconstant domain semantics to varying domain semantics.
In this paper we focus on the core aspect of our work related to
AI: proof automation with HOL-ATPs (cf. aspects (ii)–(iv) above).
The particular contributions of this paper are as follows: In Sec. 2
we present an elegant embedding of HOML [21, 25] in HOL [5, 7].
This background theory extends and adapts the work as presented
in [9, 10]. In Sec. 3, we present details on the encoding of this embedding and of Gödel’s argument in the concrete THF syntax [33]for HOL, and we report on the experiments we have conducted with
HOL-ATPs. The main findings of these experiments are summarized
in Sec. 4. Related and future work is addressed in Sec. 5, and thepaper is concluded in Sec. 6. None of the above aspects have beenaddressed (at least not in depth) in any of our other existing (shortand partly non-reviewed) publications on the subject [12, 13, 14, 34].

2 THEORY FRAMEWORK
An embedding of quantified modal logic (with first-order and propositional quantifiers) in HOL has been presented in [10]. The theory below extends this work: quantifiers for all types are now supported, and nested uninterpreted predicate and function symbols ofarbitrary types are allowed as opposed to allowing top-level uninterpreted predicate symbols over individual variables only.

2.1 Higher-order modal logic
A notion of HOML is introduced that extends HOL with a modal operator !. An appropriate notion of semantics for HOML is obtainedby adapting Henkin semantics for HOL (cf. [24] and [21]). The presentation in this section is adapted from [25] and [5].
Def. 1 The set T of simple types is freely generated from the setof basic types {o, µ} (o stands for Booleans and µ for individuals)
using the function type constructor !. We may avoid parentheses,and α ! α ! α then stands for (α ! (α ! α)), that is, function types
associate to the right.
Def. 2 The grammar for HOML is:
s, t

::=

pα | Xα | (λXα sβ )α!β | (sα!β tα )β | (¬o!o so )o |((∨o!o!o so ) to )o | (∀(α!o)!o (λXα so ))o | (!o!o so )o3

All sources of our formalization are publicly available at https://github.com/FormalTheology/GoedelGod. Our work has attracted major public interest, and leading media institutions worldwide have reported
on it; some exemplary links to respective media reports and interviews areavailable at the above URL (see ‘Press’ subfolder).

where α, β ∈ T . pα denotes typed constants and Xα typed variables(distinct from pα ). Complex typed terms are constructed via abstraction and application. The type of each term is given as a subscript.
Terms so of type o are called formulas. The logical connectives ofchoice are ¬o!o , ∨o!o!o , ∀(α!o)!o (for α ∈ T ), and !o!o . Type subscripts may be dropped if irrelevant or obvious. Similarly, parentheses may be avoided. Binder notation ∀Xα so is used as shorthandfor ∀(α!o)!o (λXα so ), and infix notation s ∨ t is employed instead of((∨s) t). From the above connectives, other logical connectives, suchas ⊤, ⊥, ∧, ⊃, ≡, ∃, and !, can be defined in the usual way.
Def. 3 Substitution of a term Aα for a variable Xα in a term Bβ isdenoted by [A/X]B. Since we consider α-conversion implicitly, we
assume the bound variables of B avoid variable capture.
Def. 4 Two common relations on terms are given by β-reduction andη-reduction. A β-redex has the form (λX s)t and β-reduces to [t/X]s.
An η-redex has the form (λX sX) where variable X is not free in s; itη-reduces to s. We write s =β t to mean s can be converted to t by aseries of β-reductions and expansions. Similarly, s =βη t means s canbe converted to t using both β and η. For each sα ∈ HOML there is aunique β-normal form and a unique βη-normal form.
Def. 5 A frame D is a collection {Dα }α∈T of nonempty sets Dα , suchthat Do = {T, F} (for truth and falsehood). The Dα!β are collectionsof functions mapping Dα into Dβ .
Def. 6 A variable assignment g maps variables Xα to elements inDα . g[d/W] denotes the assignment that is identical to g, except forvariable W, which is now mapped to d.
Def. 7 A model for HOML is a quadruple M = ⟨W, R, D, {Iw }w∈W ⟩,where W is a set of worlds (or states), R is an accessibility relation
between the worlds in W, D is a frame, and for each w ∈ W, {Iw }w∈W
is a family of typed interpretation functions mapping constant symbols pα to appropriate elements of Dα , called the denotation of pα inworld w (the logical connectives ¬, ∨, ∀, and ! are always given thestandard denotations, see below). Moreover, it is assumed that thedomains Dα!α!o contain the respective identity relations on objectsof type α (to overcome the extensionality issue discussed in [4]).
Def. 8 The value ∥sα ∥ M,g,w of a HOML term sα on a model M =⟨W, R, D, {Iw }w∈W ⟩ in a world w ∈ W under variable assignment g isan element d ∈ Dα defined in the following way:
1. ∥pα ∥ M,g,w = Iw (pα ) and ∥Xα ∥ M,g,w = g(Xα )2. ∥(sα!β tα )β ∥ M,g,w = ∥sα!β ∥ M,g,w (∥tα ∥ M,g,w )3. ∥(λXα sβ )α!β ∥ M,g,w = the function f from Dα to Dβ such thatf (d) = ∥sβ ∥ M,g[d/Xα ],w for all d ∈ Dα
4. ∥(¬o!o so )o ∥ M,g,w = T iﬀ ∥so ∥ M,g,w = F
5. ∥((∨o!o!o so ) to )o ∥ M,g,w = T iﬀ ∥so ∥ M,g,w = T or ∥to ∥ M,g,w = T
6. ∥(∀(α!o)!o (λXα so ))o ∥ M,g,w = T iﬀ for all d ∈ Dα we have∥so ∥ M,g[d/Xα ],w = T
7. ∥(!o!o so )o ∥ M,g,w = T iﬀ for all v ∈ W with wRv we have∥so ∥ M,g,v = T
Def. 9 A model M = ⟨W, R, D, {Iw }w∈W ⟩ is called a standard modeliﬀ for all α, β ∈ T we have Dα!β = { f | f : Dα −→ Dβ }. In a
Henkin model function spaces are not necessarily full. Instead it is
only required that Dα!β ⊆ { f | f : Dα −→ Dβ } (for all α, β ∈ T ) andthat the valuation function ∥·∥ M,g,w from above is total (i.e., every term
denotes). Any standard model is obviously also a Henkin model. We
consider Henkin models in the remainder.

C. Benzmüller and B. Woltzenlogel Paleo / Automating Gödel’s Ontological Proof of God’s Existence with HOL-ATPs

Def. 10 A formula so is true in model M for world w under assignment g iﬀ ∥so ∥ M,g,w = T ; this is also denoted as M, g, w |= so . A
formula so is called valid in M iﬀ M, g, w |= so for all w ∈ W and all
assignments g. Finally, a formula so is called valid, which we denoteby |= so , iﬀ so is valid for all M. Moreover, we write Γ |= ∆ (for setsof formulas Γ and ∆) iﬀ there is a model M = ⟨W, R, D, {Iw }w∈W ⟩, an
assignment g, and a world w ∈ W, such that M, g, w |= so for allso ∈ Γ and M, g, w |= to for at least one to ∈ ∆.
The above definitions introduce higher-order modal logic K. In order to obtain logics KB and S5 respective conditions on accessibility
relation R are postulated: R is a symmetric relation in logic KB, and
it is an equivalence relation in logic S5. If these restriction apply, we
use the notations |=KB and |=S 5 . Gödel’s argument has been developedand studied in the context of logic S5 (and logic S5 has subsequently
been criticized). However, the HOL-ATPs discovered (cf. Sec. 4) that
logic KB is suﬃcient.
An important issue for quantified modal logics is whether constantdomain or varying domain semantics is considered. The theory above
introduces constant domains. Terms (other than those of Booleantype) are modeled as rigid, that is, their denotation is fixed for all
worlds. An adaptation to varying or cumulative domains is straightforward (cf. [20]). Moreover, non-rigid terms could be modeled; thatis, terms whose denotation may switch from world to world. The respective assumptions of Gödel are not obvious to us.

2.2 Classical higher-order logic
HOL is easily obtained from HOML by removing the modal operator! from the grammar, and by dropping the set of possible worlds W
and the accessibility relation R from the definition of a model. Nevertheless, we explicitly state the most relevant definitions for the particular notion of HOL as employed in this paper. One reason is that
we do want to carefully distinguish the HOL and HOML languages
in the remainder (we use boldface fonts for HOL and standard fontsfor HOML). There is also a subtle, but harmless, diﬀerence in the
HOL language as employed here in comparison to the standard presentation: here three base types are employed, whereas usually only
two base types are considered. The third base type plays a crucialrole in our embedding of HOML in HOL.
Def. 11 The set T of simple types freely generated from a set of basic
types {o, µ, ι} using the function type constructor !. o is the type of
Booleans, µ is the type of individuals, and type ι is employed as thetype of possible worlds below. As before we may avoid parentheses.
Def. 12 The grammar for higher-order logic HOL is:
s, t

::=

pα | Xα | (λXα sβ )α!β | (sα!β t α )β | ¬ o!o s o |((∨ o!o!o s o) t o) | ∀(α!o)!o(λXα s o)where α, β ∈ T. The text from Def. 2 analogously applies, except that
we do not consider the modal connectives ! and !.
The definitions for substitution (Def. 3), β- and η-reduction(Def. 4), frame (Def. 5), and assignment (Def. 6) remain unchanged.
Def. 13 A model for HOL is a tuple M = ⟨D, I⟩, where D is a frame,
and I is a family of typed interpretation functions mapping constantsymbols pα to appropriate elements of Dα , called the denotation ofpα (the logical connectives ¬, ∨, and ∀ are always given the standard denotations, see below). Moreover, we assume that the domains
Dα!α!o contain the respective identity relations.

95

Def. 14 The value ∥sα ∥ M,g of a HOL term sα on a model M = ⟨D, I⟩
under assignment g is an element d ∈ Dα defined in the followingway:
1. ∥ pα ∥ M,g = I(pα ) and ∥Xα ∥ M,g = g(Xα )2. ∥(sα!β t α )β ∥ M,g = ∥sα!β ∥ M,g (∥t α ∥ M,g )3. ∥(λXα sβ )α!β ∥ M,g = the function f from Dα to Dβ such thatf (d) = ∥sβ ∥ M,g[d/Xα ] for all d ∈ Dα
4. ∥(¬ o!o s o) o∥ M,g = T iﬀ ∥s o∥ M,g = F
5. ∥((∨ o!o!o s o) t o) o∥ M,g = T iﬀ ∥s o∥ M,g = T or ∥t o∥ M,g = T
6. ∥(∀(α!o)!o(λXα s o)) o∥ M,g = T iﬀ for all d ∈ Dα we have∥s o∥ M,g[d/Xα ] = T
The definition for standard and Henkin models (Def. 9), and fortruth in a model, validity, etc. (Def. 10) are adapted in the obvious
way, and we use the notation M, g |= s o, |= s o, and Γ |= ∆. As for
HOML, we assume Henkin semantics in the remainder.

2.3

HOML as a fragment of HOL

The encoding of HOML in HOL is simple: we identify HOML formulas of type o with certain HOL formulas of type ι ! o. The HOL
type ι ! o is abbreviated as σ in the remainder. More generally, wedefine for each HOML type α ∈ T the associated raised HOL type⌈α⌉ as follows: ⌈µ⌉ = µ, ⌈o⌉ = σ = ι ! o, and ⌈α ! β⌉ = ⌈α⌉ ! ⌈β⌉.
Hence, all HOML terms are rigid, except for those of type o.

Def. 15 HOML terms sα are associated with type-raised HOL terms⌈sα ⌉ in the following way:⌈pα ⌉ = p⌈α⌉⌈Xα ⌉ = X⌈α⌉⌈(sα!β tα )⌉ = (⌈sα!β ⌉ ⌈tα ⌉)⌈(λXα sβ )⌉ = (λ⌈Xα ⌉ ⌈sβ ⌉)˙ σ!σ ⌈sα ⌉)⌈(¬o!o so )⌉ = (¬˙ σ!σ!σ ⌈sα ⌉) ⌈tα ⌉)⌈((∨o!o!o so ) to )⌉ = ((∨⌈((∀(α!o)!o (λXα sβ )⌉ = (∀˙ (α!σ)!σ (λ⌈Xα ⌉ ⌈sβ ⌉)˙ σ!σ ⌈so ⌉)⌈(!o!o so )⌉ = (!
˙ and !
˙ ∀,˙ are the type-raised modal HOL connectives asso¬,
˙ ∨,ciated with the corresponding modal HOML connectives. They aredefined as follows (where rι!ι!o is a new constant symbol in HOL
associated with the accessibility relation R of HOML):¬
˙ σ!σ = λsσ λWι ¬ (s W)˙ σ!σ!σ = λsσ λt σ λWι s W ∨ t W∨∀˙ (α!σ)!σ = λsα!σ λWι ∀Xα s X W

˙ σ!σ = λsσ λWι ∀Vι ¬(rι!ι!o W V) ∨ s V!

˙ α sσ as shorthand for ∀˙ (α!σ)!σ (λXα sσ ).
As before, we write ∀X˙ α sσ is used˙ and ∃˙ (∃X
˙ ⊃,
˙ ⊥,
˙ ∧,
˙ ≡,
˙ !,
Further operators, such as ⊤,as shorthand for ∃˙ (α!σ)!σ (λXα sσ )) can now be easily defined.4 The
above equations can be treated as abbreviations in HOL theorem
provers. Alternatively, they can be stated as axioms where = is either
Leibniz equality or primitive equality (if additionally provided in the
HOL grammar, as is the case for most modern HOL provers).
4 We could introduce further modal operators, such as the diﬀerence modality

D, the global modality E, nominals with !, and the @ operator (cf. [10]).

96

C. Benzmüller and B. Woltzenlogel Paleo / Automating Gödel’s Ontological Proof of God’s Existence with HOL-ATPs

As a consequence of the above embedding we can express HOML
proof problems elegantly in the type-raised syntax of HOL. Using
rewriting or definition expanding, we can reduce these representations to corresponding statements containing only the basic HOL
connectives ¬ o!o, ∨ o!o!o, and ∀(α!o)!o.
Ex. 1 The HOML formula ! ∃Pµ!o P aµ is associated with the type
˙ µ!σ P aµ , which rewrites into the follow˙ ∃Praised HOL formula !
ing βη-normal HOL term of type σλWι ∀Vι ¬(r W V) ∨ ¬∀Pµ!σ ¬(P aµ V)
Next, we define validity of type-raised modal HOL propositions
sσ in the obvious way: sσ is valid iﬀ for all possible worlds wι wehave wι ∈ sσ , that is, iﬀ (sσ wι ) holds.
Def. 16 Validity is modeled as an abbreviation for the following λterm: valid = λsι!o ∀Wι s W (alternatively, we could define validity
simply as ∀(ι!o)!o). Instead of valid sσ we also use the notation [sσ ].
Ex. 2 We analyze whether the type-raised modal HOL for˙ µ!σ (P aµ ) is valid or not. For this, we formalize˙ ∃Pmula !
˙ µ−!σ (P aµ )], which expands into˙ ∃P
the HOL proof problem [!
∀Wι ∀Vι ¬(r W V) ∨ ¬∀Pµ!σ ¬(P aµ V). It is easy to check that
this term is valid in Henkin semantics: put P = λXµ λYι ⊤.
Theorem 1 (Soundness and Completeness) For all HOML formulas so we have:|= so iﬀ |= [⌈so ⌉]Proof sketch: The proof adapts the ideas presented in [10]. By
contraposition it is suﬃcient to show ̸|= so iﬀ ̸|= [⌈so ⌉], that is,∥so ∥ M,g,w (for some HOML model M, assignment g, and w) iﬀ∥∀Wι ⌈s o⌉ W∥ M,g (for some HOL model M and assignment g) iﬀ∥⌈s o⌉ W∥ M,g[w/W] (for some M, g, and w). We easily get the proof bychoosing the obvious correspondences between D and D, W and Dι ,I and I, g and g, R and rι!ι!o , and w and w.
!
From Theorem 1 we get the following corollaries:|=KB so|=S 5 soiﬀ

(symmetric rι!ι!o) |= [⌈so ⌉]iﬀ (equiv-rel rι!ι!o) |= [⌈so ⌉]where symmetric and equiv-rel are defined in an obvious way.
Constant domain quantification is addressed above. Techniques
for handling varying domain and cumulative domain quantificationin the embedding of first-order modal logics in HOL have been outlined in [8]. These techniques, which have also been adapted for thetheory above, cannot be presented here for space limitations.
Note that also non-rigid terms can easily be modeled by
type-raising. For example, a non-rigid HOML constant symbol
kingOfFranceµ would be mapped to a type-raised (and thus worlddepended) HOL constant symbol kingOfFranceι!µ .

3 EXPERIMENTS
The above embedding has been encoded in the concrete THF0 syntax[33] for HOL; cf. the files Quantified K/ KB/ S5.ax5 available
5 The formalization in these files slightly varies from the above theory w.r.t.

technical details. For example, a generic !-operator is introduced that canbe instantiated for diﬀerent accessibility relations as e.g. required for multimodal logic applications (cf. [10]). Moreover, since THF0 does not support
polymorphism, copies of the ∀˙ (α!σ)!σ and ∃˙ (α!σ)!σ connectives are provided only for the selected types (µ ! σ) ! σ and ((µ ! σ) ! σ) ! σ asprecisely required in Gödels’s proof. The Isabelle version [13] and the Coq
version of the encoding instead provide respective polymorphic definitions.

at https://github.com/FormalTheology/GoedelGod/tree/
master/Formalizations/THF (all files mentioned below are provided under this URL). The definition for quantifier ∀˙ ((µ!σ)!σ)!σ ,for example, is given as6
thf(mforall_indset,definition,( mforall_indset= ( ˆ [S: ( mu > $i > $o ) > $i > $o,W: $i] :! [X: mu > $i > $o] :( S @ X @ W ) ) )).

Subsequently the axioms, definitions, and theorems from Fig. 1
and some further, related problems have been encoded in THF0.
Then the THF0 compliant HOL-ATPs LEO-II [11], Satallax [17],and Nitpick [16] have been employed to automate the proof problems. LEO-II, which internally cooperates with the first-order prover
E [29], was used exclusively in the initial round of experiments, thatis, it was the first prover to automate Gödel’s ontological argument.
Theorem T1 from Fig. 1, for example, is formalized asthf(thmT1,conjecture,( v@ ( mforall_indset@ ˆ [Phi: mu > $i > $o] :( mimplies @ ( p @ Phi )@ ( mdia@ ( mexists_ind@ ˆ [X: mu] :( Phi @ X ) ) ) ) ) )).

This encodes the HOL formula˙ µ φX]˙ µ!σ p(µ!σ)!σ φ ⊃
˙ ∃X
˙!
[∀φ
v in the THF0 encoding stands for valid and p corresponds to theuppercase P, for ‘positive’, from Fig. 1. The respective encodings
and the results of a series of recent experiments with LEO-II (version 1.6.2), Satallax (version 2.7), and Nitpick (version 2013) areprovided in Fig. 2. The first row marked with T1, for example, showsthat theorem T1 follows from axioms A2 and A1 (where only the⊃-direction is needed); LEO-II and Satallax confirm this in 0.1 second. The experiments have been carried out w.r.t. the logics K and/or
KB, and w.r.t. constant (const) and varying (vary) domain semantics
for the domains of individuals. The exact dependencies (available
axioms and definitions) are displayed for each single problem. The
results of the prover calls are given in seconds. ‘—’ means timeout. ‘THM’, ‘CSA’, ‘SAT’, and ‘UNS’ are the reported result statuses; they stand for ‘Theorem’, ‘CounterSatisfiable’, ‘Satisfiable’,and ‘Unsatisfiable’, respectively. The experiments can be easily reproduced: all relevant files have been provided at the above URL.
For example, the two THF0 problem files associated with the firsttable row for T1 are T1 K const min.p and T1 K vary min.p, andthose associated with the second row for T1 are T1 K const max.p
and T1 K vary max.p, respectively. Moreover, a simple shell script
call tptp.sh is provided, which can be used to make remotecalls to LEO-II, Satallax, and Nitpick installed at Sutcliﬀe’s SystemOnTPTP infrastructure [32] at the University of Miami. The experiments used standard 2.80GHz computers with 1GB memory remotely located in Miami.
6 $i, $o, and mu represent the HOL base types i, o, and µ. $i>$o encodesa function (predicate) type. Function application is represented by @, andfor universal quantification, existential quantification and λ-abstraction thesymbols !, ? and ˆ are employed. ¬, ∨, ∧, and ⊃ are written as ˜, |, &, and=>, respectively. The type-raised modal connectives are called mforall *,mexists *, mnot, mor, mand, mimplies, etc.

97

C. Benzmüller and B. Woltzenlogel Paleo / Automating Gödel’s Ontological Proof of God’s Existence with HOL-ATPs

HOL encoding
A1
A2
T1
D1
A3
C
A4
D2
T2
D3
A5
T3

MC
FG
MT
CO
D2’
CO’

dependencies

logic

statusLEO-II
const/vary

Satallax
const/vary

Nitpick
const/vary

K
K

THM
THM

0.1/0.1
0.1/0.1

0.0/0.0
0.0/5.2

—/—
—/—

K
K

THM
THM

0.0/0.0
0.0/0.0

0.0/0.0
5.2/31.3

—/—
—/—

K
K

THM
THM

19.1/18.3
12.9/14.0

0.0/0.0
0.0/0.0

—/—
—/—

K
K
KB
KB

CSA
CSA
THM
THM

—/—
—/—
0.0/0.1
—/—

—/—
—/—
0.1/5.3—/—

3.8/6.2
8.2/7.5
—/—
—/—

˙ σ]
˙ !s
[sσ ⊃

D2, T2, T3
A1, A2, D1, A3, A4, D2, D3, A5
˙ µ!σ ∀X˙ µ (gµ!σ X ⊃˙ (¬(˙ ¬(φX)))][∀φ˙ p(µ!σ)!σ φ) ⊃˙
A1, D1A1, A2, D1, A3, A4, D2, D3, A5
˙ µ (gµ!σ X ⊃˙ µ ∀Y˙ ( gµ!σ Y ⊃˙ X=˙ Y))] D1, FG[∀X
A1, A2, D1, A3, A4, D2, D3, A5

KB
KB
KB
KB
KB
KB

THM
THM
THM
THM
THM
THM

17.9/——/—
16.5/—
12.8/15.1—/——/—

3.3/3.2—/—
0.0/0.0
0.0/5.4
0.0/3.3
—/—

—/—
—/—
—/—
—/—
—/—
—/—

∅ (no goal, check for consistency)
A1, A2, D1, A3, A4, D2, D3, A5
˙ µ (φY ⊃˙ µ!σ (ψX ⊃˙ ∀Y˙!
˙ ψY))
ess(µ!σ)!µ!σ = λφµ!σ λXµ ∀ψ∅ (no goal, check for consistency)
A1(⊃), A2, D2’, D3, A5
A1, A2, D1, A3, A4, D2’, D3, A5

KB

SAT

—/—

—/—

7.3/7.4

KB
KB

UNS
UNS

7.5/7.8
—/—

—/—
—/—

—/—
—/—

˙ µ!σ p(µ!σ)!σ (λXµ ¬(φX))˙ ¬(pφ)]˙≡˙[∀φ˙ µ!σ ∀ψ˙ µ (φX ⊃˙ µ!σ (p(µ!σ)!σ φ ∧˙!
˙ ∀X˙ ψX)) ⊃˙ pψ][∀φ
˙ µ φX]˙ µ!σ p(µ!σ)!σ φ ⊃˙ ∃X˙!
A1(⊃), A2[∀φ
A1, A2˙ µ!σ p(µ!σ)!σ φ ⊃˙ φXgµ!σ = λXµ ∀φ[ p(µ!σ)!σ gµ!σ ]˙ µ gµ!σ X]˙ ∃X
T1, D1, A3[!
A1, A2, D1, A3
˙ µ!σ p(µ!σ)!σ φ ⊃˙
˙ !pφ][∀φ˙ µ!σ (ψX ⊃˙ µ (φY ⊃
˙ ∀ψ
˙ ∀Y
˙!
˙ ψY))
ess(µ!σ)!µ!σ = λφµ!σ λXµ φX ∧˙ µ gµ!σ X ⊃˙ (ess(µ!σ)!µ!σ gX)]
A1, D1, A4, D2[∀X
A1, A2, D1, A3, A4, D2
˙ µ φY)˙ µ!σ (ess φX ⊃˙ ∃Y˙!
NEµ!σ = λXµ ∀φ[ p(µ!σ)!σ NEµ!σ ]˙ µ gµ!σ X]˙ ∃X
D1, C, T2, D3, A5[!
A1, A2, D1, A3, A4, D2, D3, A5
D1, C, T2, D3, A5
A1, A2, D1, A3, A4, D2, D3, A5

Figure 2.

HOL encodings and experiment results for Scott’s version of Gödel’s ontological argument from Fig. 1.

4 MAIN FINDINGS
Several interesting and partly novel findings have been contributedby the HOL-ATPs, including:
1. The axioms and definitions from Fig. 1 are consistent (cf. CO in
Fig. 2).
2. Logic K is suﬃcient for proving T1, C and T2.
3. For proving the final theorem T3, logic KB is suﬃcient (and for K
a countermodel is reported). This is highly relevant since several
philosophers have criticized Gödel’s argument for the use of logic
S5. This criticism is thus provably pointless.
4. Only for T3 the HOL-ATPs still fail to produce a proof directlyfrom the axioms; thus, T3 remains an interesting benchmark problem; T1, C, and T2 are rather trivial for HOL-ATPs.
5. Gödel’s original version of the proof [23], which omits conjunctφ(x) in the definition of essence (cf. D2’), seems inconsistent(cf. the failed consistency check for CO’ in Fig. 2). As far as weare aware of, this is a new result.
6. Gödel’s axioms imply what is called the modal collapse (cf. MC
in Fig. 2) φ ⊃ !φ, that is, contingent truth implies necessary truth(which can even be interpreted as an argument against free will;cf. [31]). MC is probably the most fundamental criticism put forward against Gödel’s argument.
7. For proving T1, only the ⊃-direction of A1 is needed. How-ever, the ⊂-direction of A1 is required for proving T2. Somephilosophers (e.g. [3]) try to avoid MC by eluding/replacing the⊃-direction of A1.
8. Gödel’s axioms imply a ‘flawless God’, that is, an entity that can
only have ‘positive’ properties (cf. FG in Fig. 2). However, a comment by Gödel in [23] explains that ‘positive’ is to be interpreted
in a moral aesthetic sense only.
9. Another implication of Gödel’s axioms is monotheism (see MT in
Fig. 2). MT can easily be proved by Satallax from FG and D1. It
remains non-trivial to prove it directly from Gödel’s axioms.
10. All of the above findings hold for both constant domain semantics
and varying domain semantics (for the domain of individuals).
The above findings, in particular (10), well illustrate that the theory framework from Sec. 2 has a great potential towards a flexible support system for computational theoretical philosophy. In fact,Gödel’s ontological argument has been verified and even automatednot only for one particular setting of logic parameters, but these logic
parameters have been varied and the validity of the argument has
been reconfirmed (or falsified, cf. D2’ and CO’) for the modified
setting. Moreover, our framework is not restricted to a particular theorem proving system, but has been fruitfully employed with some of
the most prominent automated and interactive theorem provers available to date.

98

C. Benzmüller and B. Woltzenlogel Paleo / Automating Gödel’s Ontological Proof of God’s Existence with HOL-ATPs

5 RELATED AND FUTURE WORK
We are pioneering the computer-supported automation of modern
versions of the ontological argument. There are two related papers[27, 28]. Both focus on the comparably simpler argument by Anselm.
[27] encodes (a variant) of Anselm’s argument in first-order logic andemploys the theorem prover PROVER9 in experiments; this work has
been criticized in [22]. The work in [28], which has evolved in parallel to ours, interactively verifies Anselm’s argument in the higherorder proof assistant PVS. Note in particular, that both formalizations
do not achieve the close correspondence between the original formulations and the formal encodings that can be found in our approach.
A particular strength of our universal logic framework is that it
can be easily adapted for logic variations and even supports flexible
combinations of logics (cf. [6]). In ongoing and future work we will
therefore investigate further logic parameters for Gödel’s argument,
including varying domains at higher types and non-rigid terms. We
plan to make the entire landscape of results available to the interested
communities. This is relevant, since philosophers are sometimes imprecise about the very details of the logics they employ.

6 CONCLUSION
While computers can now calculate, play games, translate, plan,
learn and classify data much better than we humans do, tasks involving philosophical and theological inquiries have remained mostly untouched by our technological progress up to now. Due to the abstractand sophisticated types of reasoning they require, they can be considered a challenging frontier for automated reasoning.
We accepted this challenge and decided to tackle, with automated reasoning techniques, a philosophical problem that is almost
1000 years old: the ontological argument for God’s existence, firstly
proposed by St. Anselm of Canterbury and greatly improved by
Descartes, Leibniz, Gödel and many others throughout the centuries.
So far, there was no AI system capable of dealing with such complex
problems. We created a prototypical infrastructure extending widelyused systems such as LEO-II, Satallax, and Nitpick (and Isabelle andCoq) to allow them to cope with modalities; and using the extended
systems we were able to automatically reconstruct and verify Gödel’s
argument, as well as discover new facts and confirm controversial
claims about it. This is a landmark result, with media repercussion ina global scale, and yet it is only a glimpse of what can be achievedby combining computer science, philosophy and theology.
Our work, in this sense, oﬀers new perspectives for a computational theoretical philosophy. The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility, but the computer can assist in building and checking rigorously
correct logical arguments. In case of logico-philosophical disputes,
the computer can check the disputing arguments and partially fulfill
Leibniz’ dictum: Calculemus — Let us calculate!

ACKNOWLEDGEMENTS
We thank Alexander Steen, Max Wisniewski, and the anonymous
reviewers for their comments and suggestions.

REFERENCES[1] R.M. Adams, ‘Introductory note to *1970’, in Kurt Gödel: Collected
Works Vol. 3: Unpubl. Essays and Letters, Oxford Univ. Press, (1995).
[2] A.C. Anderson and M. Gettings, ‘Gödel ontological proof revisited’,in Gödel’96: Logical Foundations of Mathematics, Computer Science,
and Physics: Lecture Notes in Logic 6, 167–172, Springer, (1996).

[3] C.A. Anderson, ‘Some emendations of Gödel’s ontological proof’,
Faith and Philosophy, 7(3), (1990).
[4] P.B. Andrews, ‘General models and extensionality’, Journal of Symbolic Logic, 37(2), 395–397, (1972).
[5] P.B. Andrews, ‘Church’s type theory’, in The Stanford Encyclopedia of
Philosophy, ed., E.N. Zalta, spring 2014 edn., (2014).
[6] C. Benzmüller, ‘HOL based universal reasoning’, in Handbook of the
4th World Congress and School on Universal Logic, ed., J.Y. Beziau etal., pp. 232–233, Rio de Janeiro, Brazil, (2013).
[7] C. Benzmüller and D. Miller, ‘Automation of higher-order logic’, in
Handbook of the History of Logic, Volume 9 — Logic and Computation, Elsevier, (2014). Forthcoming; preliminary version available at
http://christoph-benzmueller.de/papers/B5.pdf.
[8] C. Benzmüller, J. Otten, and Th. Raths, ‘Implementing and evaluating provers for first-order modal logics’, in Proc. of the 20th European
Conference on Artificial Intelligence (ECAI), pp. 163–168, (2012).
[9] C. Benzmüller and L.C. Paulson, ‘Exploring properties of normal multimodal logics in simple type theory with LEO-II’, in Festschrift in
Honor of Peter B. Andrews on His 70th Birthday, ed., C. Benzmüller etal., 386–406, College Publications, (2008).
[10] C. Benzmüller and L.C. Paulson, ‘Quantified multimodal logics in simple type theory’, Logica Universalis, 7(1), 7–20, (2013).
[11] C. Benzmüller, F. Theiss, L. Paulson, and A. Fietzke, ‘LEO-II - a cooperative automatic theorem prover for higher-order logic’, in Proc. of
IJCAR 2008, number 5195 in LNAI, pp. 162–170. Springer, (2008).
[12] C. Benzmüller and B. Woltzenlogel-Paleo, ‘Formalization, mechanization and automation of Gödel’s proof of God’s existence’,arXiv:1308.4526, (2013).
[13] C. Benzmüller and B. Woltzenlogel-Paleo, ‘Gödel’s God in Isabelle/HOL’, Archive of Formal Proofs, (2013).
[14] C. Benzmüller and B. Woltzenlogel-Paleo, ‘Gödel’s God on the computer’, in Proceedings of the 10th International Workshop on the Implementation of Logics, EPiC Series. EasyChair, (2013). Invited abstract.
[15] Y. Bertot and P. Casteran, Interactive Theorem Proving and Program
Development, Springer, 2004.
[16] J.C. Blanchette and T. Nipkow, ‘Nitpick: A counterexample generator
for higher-order logic based on a relational model finder’, in Proc. of
ITP 2010, number 6172 in LNCS, pp. 131–146. Springer, (2010).
[17] C.E. Brown, ‘Satallax: An automated higher-order prover’, in Proc. of
IJCAR 2012, number 7364 in LNAI, pp. 111 – 117. Springer, (2012).
[18] R. Corazzon.
Contemporary bibliography on ontological arguments:
http://www.ontology.co/biblio/ontological-proofcontemporary-biblio.htm.
[19] M. Fitting, Types, Tableaux and Gödel’s God, Kluwer, 2002.
[20] M. Fitting and R.L. Mendelsohn, First-Order Modal Logic, volume 277
of Synthese Library, Kluwer, 1998.
[21] D. Gallin, Intensional and Higher-Order Modal Logic, North-Holland,
1975.
[22] P. Garbacz, ‘PROVER9’s simplifications explained away’, Australasian
Journal of Philosophy, 90(3), 585–592, (2012).
[23] K. Gödel, Appx.A: Notes in Kurt Gödel’s Hand, 144–145. In [31], 2004.
[24] L. Henkin, ‘Completeness in the theory of types’, Journal of Symbolic
Logic, 15(2), 81–91, (1950).
[25] R. Muskens, ‘Higher Order Modal Logic’, in Handbook of Modal
Logic, ed., P Blackburn et al., 621–653, Elsevier, Dordrecht, (2006).
[26] T. Nipkow, L.C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, number 2283 in LNCS, Springer, 2002.
[27] P.E. Oppenheimera and E.N. Zalta, ‘A computationally-discovered simplification of the ontological argument’, Australasian Journal of Philosophy, 89(2), 333–349, (2011).
[28] J. Rushby, ‘The ontological argument in PVS’, in Proc. of CAV Workshop “Fun With Formal Methods”, St. Petersburg, Russia,, (2013).
[29] S. Schulz, ‘E – a brainiac theorem prover’, AI Communications, 15(2),111–126, (2002).
[30] D. Scott, Appx.B: Notes in Dana Scott’s Hand, 145–146. In [31], 2004.
[31] J.H. Sobel, Logic and Theism: Arguments for and Against Beliefs in
God, Cambridge U. Press, 2004.
[32] G. Sutcliﬀe, ‘The TPTP problem library and associated infrastructure’,
Journal of Automated Reasoning, 43(4), 337–362, (2009).
[33] G. Sutcliﬀe and C. Benzmüller, ‘Automated reasoning in higher-orderlogic using the TPTP THF infrastructure.’, Journal of Formalized Reasoning, 3(1), 1–27, (2010).
[34] B. Woltzenlogel-Paleo and C. Benzmüller, ‘Automated verification andreconstruction of Gödel’s proof of God’s existence’, OCG J., (2013).