Variants of Kurt G¨odel’s (1970), resp. Dana Scott’s (1972), modal ontological argument have previously been studied and verified on the computer by Benzm¨uller and Woltzenlogel-P. (2014; 2016) and Benzm¨uller and Fuenmayor (2020), and some previously unknown issues were revealed in these works,1 and it was shown that logic KB, instead of S5, is already sufficient to derive from G¨odel’s axioms that a supreme being necessarily exists.
In this paper simplified variants of G¨odel’s modal ontological argument are explored and studied. Our simplifica-tions have been developed in interaction with the proof assistant Isabelle/HOL (Nipkow, Paulson, and Wenzel 2002) and by employing Benzm¨uller’s (2019; 2013) shallow semantical embedding (SSE) approach as enabling technology. This technology supports the reuse of automated theorem proving (ATP) and model finding tools for classical higher-order logic (HOL) to represent and reason with a wide range of non-classical logics and theories, including higher-order modal logics (HOMLs) and G¨odel’s modal ontological argument, which are in the focus of this paper.
One of the new, simplified modal arguments is as follows. The notion of being Godlike (G) is exactly as in G¨odel’s original work. Thus, a Godlike entity, by definition, possesses all positive properties (P is an uninterpreted constant denoting positive properties):
The three only axioms of the new theory which constrain the interpretation of G¨odel’s positive properties (P) are:
Self-difference is not a positive property.2
A property entailed or necessarily entailed by a positive property is positive.
A3 The conjunction of any collection of positive properties is positive.3
Technical reading: if Z is any set of positive properties, then the property X obtained by taking the conjunction of the properties in Z is positive.
In these premises the following defined symbols are used, where is a possibilist second-order quantifier and where
is an actualist first-order quantifier for individuals:
From and A3 it follows, in a few argumentation steps in modal logic K, that a Godlike entity possibly and necessarily exists. Modal collapse, which expresses that there are no contingent truths and which thus eliminates the possibility of alternative possible worlds, does not follow from these axioms. Also monotheism is not implied. These observations should render the new theory interesting to theoretical philosophy and theology.
Compare the above with G¨odel’s premises of the modal ontological argument (in the consistent variant of Scott):
A1 One of a property or its complement is positive.
A2 A property necessarily entailed by a positive property is positive.
A3 The conjunction of any collection of positive properties is positive (or, alternatively, being Godlike is a positive property).
A4 Any positive property is necessarily positive.
A5 Necessary existence (NE) is a positive property.
in logic KB instead of just K.4 (Remember that logic S5 is not needed.)
(all other definitions are as before):
Informally: Property Y is an essence E of an entity x if, and only if, (i) Y holds for x and (ii) Y necessarily entails every property Z of x. Moreover, an entity x has the property of necessary existence if, and only if, the essence of x is necessarily instantiated.
Using G¨odel’s premises as stated it can be proved automatically that a Godlike entity possibly and necessarily exists (Benzm¨uller and Woltzenlogel Paleo 2016). However, modal collapse is still implied even in the weak logic KB.5
Benzm¨uller and Fuenmayor (2020) recently showed that different modal ultrafilter properties can be deduced from G¨odel’s premises. These insights are key to the argument simplifications developed and studied in this paper: If G¨odel’s premises entail that positive properties form a modal ultrafilter, then why not turning things around, and start out with an axiom U1 postulating ultrafilter properties for P? Then use U1 instead of other axioms for proving that a Godlike entity necessarily exists, and on the fly explore what further simplifications of the argument are triggered. This research plan worked out and it led to simplified argument variants as presented above and in the remainder.
The proof assistant Isabelle/HOL and its integrated ATP systems have supported our exploration work surprisingly well, despite the undecidability and high complexity of the underlying logic setting. As usual, we here only present the main steps of the exploration process, and various interesting eureka or frustration steps in between are dropped.
The structure of this paper is as follows: An SSE of HOML in HOL is introduced in Sect. 2. This section, parts of which have been adapted from Kirchner et al. (2019), ensures that the paper is sufficiently self-contained; readers familiar with the SSE approach may simply skip it. Modal fil-ter and ultrafilter are defined in Sect. 3. Section 4 recaps, in some more detail, the G¨odel/Scott variant of the modal ontological argument from above. Subsequently, an ultrafilter-based modal ontological argument is presented in Sect. 5. This new argument is further simplified in Sect. 6, leading to our proposal based on axioms and A3 as presented before. Further simplifications and modifications are studied in Sect. 7, and related work is discussed in Sect. 8.
Since we develop, explain and discuss our formal encodings directly in Isabelle/HOL, some familiarity with this proof assistant and its underlying logic HOL (Andrews 2002; Benzm¨uller and Andrews 2019) is assumed. The entire sources6 of our formal encodings are presented and explained in detail in this paper.
The contributions of this paper are thus manifold. Besides the novel variants of the modal ontological argument that we contribute to metaphysics and theology, we demonstrate how the SSE technique, in combination with higher-order reasoning tools, can be employed in practical studies to explore such new knowledge. Moreover, we contribute useful source encodings that can be reused and adapted to teach quantified modal logics in interdisciplinary lecture courses.
Various SSEs of quantified non-classical logics in HOL have been developed, studied and applied in related work, cf. Benzm¨uller (2019) and Kirchner et al. (2019) and the references therein. These contributions, among others, show that the standard translation from propositional modal logic to first-order (FO) logic can be concisely modeled (i.e., embedded) within HOL theorem provers, so that the modal operator 2, for example, can be explicitly defined by the -term
, where R denotes the accessibility relation associated with 2. Then one can construct FO formulas involving
and use them to represent and proof theorems. Thus, in an SSE, the target logic is internally represented using higher-order (HO) constructs in a theorem proving system such as Isabelle/HOL. Benzm¨uller
and Paulson (2013) developed an SSE that captures quan-tified extensions of modal logic. For example, if is shorthand in HOL for
, then
would be represented as
, where
stands for the
-term
, and the 2 gets resolved as above. To see how these expressions can be resolved to produce the right representation, consider the following series of reductions:
Thus, we end up with a representation of in HOL. Of course, types are assigned to each (sub-)term of the HOL language. We assign individual terms (such as variable x above) the type e, and terms denoting worlds (such as variable w above) the type i. From such base choices, all other types in the above presentation can actually be inferred. An explicit encoding of HOML in Isabelle/HOL, following the above ideas, is presented in Fig. 1.7 In lines 4–5 the base types i and e are declared (text passages in red are comments). Note that HOL comes with an inbuilt base type bool, the bivalent type of Booleans. No cardinality constraints are associated with types i and e, except that they must be non-empty. To keep our presentation concise, useful type synonyms are introduced in lines 6–9.
abbreviates the type
is the function type constructor in HOL), and terms of type
can be seen to represent world-lifted propositions, i.e., truth-sets in Kripke’s modal relational semantics (Garson 2018). The explicit transition from modal propositions to terms (truth-sets) of type
is a key aspect of the SSE technique, and in the remainder of this article we use phrases such as “world-lifted” or “
-type” terms to emphasize this conversion in the SSE approach.
, which stands for
, is the type of world-lifted, intensional properties.
and
, which abbreviate
and
, are the types associated with unary and binary modal logic connectives. The modal logic connectives are defined in lines 12–25. In line 16, for example, the definition of the world-lifted
-connective of type
is given; explicit type information is presented after the ::-token for ‘c5’, which is the ASCIIdenominator for the (right-associative) infix-operator
as
Figure 1: SSE of HOML in HOL.
introduced in parenthesis shortly after. is then de-fined as abbreviation for the truth-set
, respectively. In the remainder we generally use bold-face symbols for world-lifted connectives (such as
) in order to rigorously distinguish them from their ordinary counterparts (such as
) in meta-logic HOL.
Further modal logic connectives, such as , and
are introduced analogously. The operator
, introduced in lines 22–23, is inverting properties of types
; this operation occurs in G¨odel’s axiom A1. = and
are defined
in lines 24–25 as world-independent, syntactical equality.
The world-lifted modal 2-operator is introduced in lines 19–20; accessibility relation R is now synonymously named r in infix notation. The definition of 3 is analogous.
The world-lifted (polymorphic) possibilist quantifier as discussed before is introduced in line 28–29. In line 30, user-friendly binder-notation for
is additionally defined. Instead of distinguishing between
and
as in our illustrating example,
-symbols are overloaded here. The introduction of the possibilist
-quantifier is analogous.
Additional actualist quantifiers, and
, are introduced in lines 36–42. Their definition is guarded by an explicit, possibly empty, existsAt (@) predicate, which encodes whether an individual object actually “exists” at a particular world, or not. The actualist quantifiers are declared non-polymorphic, and they support quantification over individuals only. In the remainder we will indeed apply
and
for different types in the type hierarchy of HOL, while
and
exclusively quantify over individuals only.
Global validity of a world-lifted formula , denoted as
, is introduced in line 45 as an abbreviation for
.
Consistency of the introduced concepts is confirmed by the model finder nitpick (Blanchette and Nipkow 2010) in line 48. Since only abbreviations and no axioms have been introduced so far, the consistency of the Isabelle/HOL theory HOML as displayed in Fig. 1 is actually evident.
In line 49–52 it is studied whether instances of the Barcan and the converse Barcan formulas are implied. As expected, both principles are valid only for possibilist quantification, while they have countermodels for actualist quantification.
Lines 54–55 declare some specific parameter settings for some of the reasoning tools that we employ.
Theorem 1. The SSE of HOML in HOL is faithful (for K).
Proof. Analagous to Benzm¨uller and Paulson (2013).
Theory HOML thus models base logic K in HOL. Axiom B, see above, can be postulated to arrive at logic KB.
Theory MFilter, for “modal filter”, see Fig. 2, imports theory HOML and adapts the topological notions of filter and ultra-filter to our modal logic setting. For an introduction to the notions of filter and ultrafilter see the literature, e.g., (Burris and Sankappanavar 1981) or also (Odifreddi 2000). Our notion of modal ultrafilter is introduced in lines 20–21 as a world-lifted characteristic function of type . A modal ultrafilter is thus a world-dependent set of intensions of
-type properties; in other words, a
-subset of the
-powerset of
-type property extensions. A modal ultrafilter
is defined as a modal filter satisfying an additional maximality condition:
, where
is elementhood of
-type objects in
-sets of
-type objects (see lines 3–4), and where
is the relative set complement operation on sets of entities (line 11). A modal filter
, see lines 14–17, is required to
1. be large: U , where U denotes the full set of
-type objects we start with,
Figure 2: Definition of filter and ultrafilter (for possible worlds).
2. exclude the empty set: , where
is the world-lifted empty set of
-type objects,
3. be closed under supersets: (the world-lifted
-relation is defined in lines 7– 8), and
4. be closed under intersections: (where
is defined in lines 9–10).
Benzm¨uller and Fuenmayor (2020) have studied two different notions of modal ultrafilter (termed - and
-ultrafilter), which are defined on intensions and extensions of properties, respectively. This distinction is not needed in this paper; what we call modal ultrafilter here corresponds to their notion of
-ultrafilter.
We start out in Fig. 3 with the introduction of some basic abbreviations and definitions for the G¨odel/Scott variant of the modal ontological argument. This theory file, which is termed BaseDefs and which imports HOML, is reused without modification also in all other variants as explored in this paper later on. In line 4 the uninterpreted constant symbol P, for “positive properties”, is declared; it has type . P thus denotes an intensional, world-depended concept. In lines 7–11 abbreviations for the previously discussed relations and predicates
,
and Pos are introduced. In lines 14–15, G¨odel’s notion of “being Godlike” (G) is de-fined, and in lines 18–21 the previously discussed definitions for Essence (E) and Necessary Existence (NE) are given. The full formalization of Scott’s variant of G¨odel’s argument is presented as theory ScottVariant in Fig. 4. This theory imports and relies on the previously introduced notions from theory files HOML, MFilter and BaseDefs. The premises of G¨odel’s argument, as already discussed
Figure 3: Definitions for all variants discussed in the remainder.
earlier, are stated in lines 4–10. In line 12 a semantical counterpart (symmetry of the accessibility relation r associated with the 2-operator) of the B axiom is proved.
An abstract level “proof net” for theorem T6, the necessary existence of a Godlike entity, is presented in lines 15– 25. Following the literature, the proof goes as follows: From A1 and A2 infer T1: positive properties are possibly exem-plified. From A3 and the defn. of G obtain T2: being Godlike is a positive property (Scott actually directly postulated T2). Using T1 and T2 show T3: possibly a Godlike entity exists. Next, use A1, A4, the defns. of G and E to infer T4: being Godlike is an essential property of any Godlike entity. From this, and the defns. of G, and NE have T5: the possible existence of a Godlike entity implies its necessary existence. T5 and T3 then imply T6.
The five subproofs and their dependencies have been automatically proved using state-of-the-art ATP system integrated with Isabelle/HOL via its sledgehammer tool; sledgehammer then identified and returned the abstract level proof justifications as displayed here, e.g. “using T1 T2 by simp”. The mentioned proof engines/tactics blast, metis, and simp are trustworthy components of Isabelle/HOL’s, since they internally reconstruct and check each (sub-)proof in the proof assistants small and trusted proof kernel. The smt method, which relies on an external satisfiability modulo solver (CVC4 in our case), is less trusted, but we nevertheless use it here since it was the only Isabelle/HOL method that was able to close this subproof in a single step (we want to avoid displaying longer interactive proofs due to space restrictions). Using the defns. from Sect. 2, one can generally reconstruct and verify all presented proofs with pen and paper directly in meta-logic HOL. Moreover, reconstruction of modal logic proofs from such proof nets within direct proof calculi for quantified modal logics, cf. Kanckos and Woltzenlogel-P. (2017) or Fitting (2002) is also possible.
The presented theory is consistent, which is confirmed in line 31 by model finder nitpick; nitpick reports a model consisting of one world and one Godlike entity.
Figure 4: G¨odel’s modal ontological argument; Scott’s variant.
Figure 5: Ultrafilter variant.
Validity of modal collapse (MC) is confirmed in lines 34– 42; a proof net displaying the proofs main idea is shown.
Most relevant for this paper is that the ATP systems were able to quickly prove that G¨odel’s notion of positive properties P constitutes a modal ultrafilter, cf. lines 45–55. This was key to the idea of taking the modal ultrafilter property of P as an axiom U1 of the theory; see the next section.
In lines 57–60 some further relevant lemmata are proved. And in line 62–70 we hint at a much simpler, alternative proof argument: Take the set HF G of all supersets of G; it follows from G¨odel’s theory that this set is a modal filter (line 66) resp. modal ultrafilter (line 67), i.e., HF G is the modal Hauptfilter of G. The necessary existence of a Godlike entity now becomes a simple corollary of this result (see line 70, where T6Again is proved exclusively from F1). In Sect. 7 we will later present an argument variant that is based on this observation.8
Taking U1 as an axiom for G¨odel’s theory in fact leads to a significant simplification of the modal ontological argument; this is shown in lines 10–17 of the theory file UFilterVariant in Fig. 5: not only G¨odel’s axiom A1 can be dropped, but also axioms A4 and A5, together with defns. E and NE. Even logic KB can be given up, since K is now sufficient for verifying the proof argument.
The proof is similar to before: Use U1 and A2 to infer T1 (positive properties are possibly exemplified). From A3 and defn. of G have T2 (being Godlike is a positive property). T1 and T2 imply T3 (a Godlike entity possibly exists). From U1, A2, T2 and the defn. of G have T5 (possible existence of a Godlike entity implies its necessary existence). Use T5 and T3 to conclude T6 (necessary existence of a Godlike entity).
Consistency of the theory is confirmed in line 20; again a model with one world and one Godlike entity is reported.
Most interestingly, modal collapse MC now has a simple countermodel as nitpick informs us in line 23. This countermodel consists of a single entity and two worlds
and
with accessibility relation
. Trivially, formula
is such that
holds in
but not in
, which invalidates MC at world
is the Godlike entity in both worlds, i.e., G is the property that holds for
in
and
, which we may denote as
. Using tuple notation we may write
.
Remember that P, which is of type , is an intensional, world-depended concept. In our countermodel for MC in line 23 the extension of P for world
has the above G and
as its elements, while in world
we have G and
. Using tuple notation we may note P as
In order to verify that P is a modal ultrafilter we have to check whether the respective modal ultrafilter conditions are satisfied in both worlds. U in
and also in
, since both
and
are in
in
and also in
, since both
and
are not in P. It is also easy to verify that P is closed under supersets and intersection in both worlds.
Note that in our countermodel for MC, also G¨odel’s axiom A4 is invalidated. Consider , i.e., X is true for
in
, but false for
in
. We have P X in
, but we do not have 2(P X) in
, since P X does not hold in
, which is reachable in r from
.
nitpick is capable of computing all partial modal ultrafil-ters as part of its countermodel exploration: out of 512 candidates, nitpick identifies 32 structures of form , for
, in which F satisfies the ultrafilter conditions in the specified world i. An example for such an
is
F is not a proper modal ultrafilter, since F fails to be an ultrafilter in world .
What modal ultrafilters properties of P are actually needed to support T6? Which ones can be dropped? Experiments with our framework, as displayed in theory file SimpleVariant in Fig. 6, confirm that only the filter conditions from Sect. 3 must be upheld for P; maximality can be dropped. However, it is possible to merge filter condition 3 (closed under supersets) for P with G¨odel’s A2 into axiom as shown in line 6 of Fig. 6. Moreover, instead of requiring that the empty set
must not be a positive property, we postulate that self-difference
is not (line 5); note that self-difference is extensionally equal to
. Selfidentity and self-difference have been used frequently in the history of the ontological argument, which is part of the mo-
Figure 6: Simplified variant.
tivation for this switch. As intended, filter condition 4 is now implied by the theory (see theorem F1 proved in line 31), as well as positiveness of self-identity (line 10). The essential idea of the theory SimpleVariant in Fig. 6 is to show that it actually suffices, in combination with A3, to postulate that P is a modal filter, and this is what our simplified axioms do.
From the definition of G and the axioms and A3 (lines 5–7) theorem T6 immediately follows: in line 13 several theorem provers integrated with sledgehammer quickly report a proof (
1sec). Moreover, a more detailed and more intuitive “proof net” is presented in lines 14–18; the proof argument is analogous to what has been discussed before.
In lines 21–23, countermodels for modal collapse MC (similar to the one discussed before) and for monotheism MT are reported.
Further questions are answered experimentally (lines 26– 38): neither A1, nor A4 or A5, of the premises we dropped from G¨odel’s theory are implied anymore, all have countermodels. In lines 31–32 we see that P is still a filter, but not an ultrafilter. Since some of these axioms, e.g. G¨odel’s strong A1, have been discussed controversially in the history of G¨odel’s argument, and since MC and MT are independent, we have arrived at a philosophically and theologically potentially relevant simplification of G¨odel’s work.
Postulating T2 instead of A3 Instead of working with third-order axiom A3 to infer T2 as in theory SimpleVariant,
Figure 7: Simplified variant with axiom
Figure 8: Simplified variant with simple entailment in logic K.
we directly postulate T2 as an axiom in theory SimpleVariantPG; cf. the new axiom T2 in line 7 of in Fig. 7.
Theorem T6 can be proved essentially as before (lines 10– 15), and MC and MT still have countermodels (lines 20–22).
Simple Entailment in Axiom Instead of using a disjunction of simple entailment and necessary entailment in axiom
we may in fact only require simple entailment in
; see axiom
(line 6) of the theory file SimpleVariantSE displayed in Fig. 8. Proofs for T6, the necessary existence of a Godlike entity, and also T7, existence of a Godlike entity, can still be quickly found (lines 10–11).
However, after replacing by
(the possible existence of a Godlike entity) is no longer implied; see line 14. As nitpick informs us, T3 now has an undesired countermodel consisting of one single world that is not connected to itself. By assuming modal axiom T (what is necessary true is true in the given world) this countermodel can be eliminated so that T3 is implied as desired (lines 16–18).
Figure 9: Simplified variant with simple entailment in logic T.
Simple Entailment in Logic T The above discussion motivates a further alternative of the simplified modal ontological argument; see theory file SimpleVariantSEinT in Fig. 9. This argument is assuming modal logic T (which comes with axiom T as discussed above), and, as before, it postulates axioms and T2 (lines 5–7):
Self-difference is not a positive property.
A property entailed by a positive property is positive.
T2 Being Godlike is a positive property.
One possible proof argument for T6 is as before; see lines 15–19. However, there is also a much simpler proof, see lines 23–30, which we explain in more detail (this simple proof is applicable to previous variants as well; it is also key to proving T5 from and T2/A3 in previous variants, including the simplified variant in Fig. 6):9
L1 The existence of a non-exemplified positive property implies that self-difference is a positive property—This follows from axiom .
L2 There is no non-exemplified positive property—From L1 and axiom .
T1’ Positive properties are exemplified—Equivalent to L2. T3’ A Godlike entity exists—Fromand axiom T2.
L3 A Godlike entity possibly exists—From and
(contrapositive of axiom T); note that L3 is not needed to obtain T6 in the next step; generally, axiom T (resp. its contrapositive
) is only needed for deriving T3/L3.
Figure 10: Hauptfiltervariant.
T6 A Godlike entity necessarily exists—From by necessitation.
Hauptfiltervariant Another drastically simplified variant of the modal ontological argument is related to the observations discussed earlier at the end of Sec. 4. There it has been shown that the set HF G, consisting of all supersets of G, is a modal filter (so that HF G is the Hauptfilter of G); this then directly implies the necessary existence of a Godlike entity. A new variant based on this observation is presented in theory file SimpleVariantHF in Fig. 10. Here the set of all supersets HF G of property G (being Godlike) is postulated to be a modal filter (axiom F1 in line 7).10 The existence and necessary existence of a Godlike entity then directly follows from F1, see lines 10–16. And as already observed before, the possible existence of a Godlike entity is independent, but can be enforced by postulating modal axiom T (lines 19– 24). Moreover, the theory is consistent (line 26) and neither modal collapse nor monotheism are implied (lines 29–30).
Fitting (2002) suggested to carefully distinguish between intensions and extensions of positive properties in the context of G¨odel’s modal ontological argument, and, in order to do so within a single framework, he introduced a suf-ficiently expressive HOML enhanced with means for the explicit representation of intensional terms and their extensions; cf. also the intensional operations used by Fuenmayor and Benzm¨uller (2017; 2020) in their formal study of the works of Fitting and Anderson (1990; 1996).
The application of computational methods to philosophical problems was initially limited to first-order theorem provers. Fitelson and Zalta (2007) used PROVER9 to find a proof of the theorems about situation and world theory in (Zalta 1993) and they found an error in a theorem about Plato’s Forms that was left as an exercise in (Pelletier and Zalta 2000). Oppenheimer and Zalta (2011) discovered, using Prover9, that one of the three premises used in their reconstruction of Anselm’s ontological argument (Oppen- heimer and Zalta 1991) was sufficient to derive the conclusion. The first-order conversion techniques that were developed and applied in these works are outlined in some detail in related work by Alama, Oppenheimer and Zalta (2015).
More recent related work makes use of higher-order proof assistants. Besides the already mentioned work of Benzm¨uller and colleagues, this includes Rushby’s (2018) study on Anselm’s ontological argument in the PVS system and Blumson’s (2017) related study in Isabelle/HOL.
The development of G¨odel’s ontological argument has recently been addressed by Kanckos and Lethen (2019). They discovered previously unknown variants of the argument in G¨odel’s Nachlass, whose relation to the presented simplified variants should be further investigated in future work.11
Related work also includes Odifreddi’s (2000) discussion on ultrafilters, dictators and God, which I was pointed to by a reviewer.
The simplifications of G¨odel’s theory as presented are far reaching. In fact, one may ask “Is this really what G¨odel had in mind?”, or are there some technical issues, such as the alternative proof in lines 22–30 from Fig. 9, that have been ignored so far? Moreover, is the definition of property entailment () really adequate in the context of the modal ontological argument, or shouldn’t this definition be replaced by concept containment, so that self-difference, resp. the empty property, would no longer
-entail any other property?12
Moreover, assuming that the simplified theory SimpleVariant from Fig. 6 is indeed still in line with what G¨odel had in mind, why not presenting the definitions and axioms using an alternative wording, for example, as follows (where we replace “positive property” by “rational/consistent property” and “Godlike entity” by “maximally-rational entity”):
G An entity x is maximally-rational (G) iff it has all rational/consistent properties.
Self-difference is not a rational/consistent property.
A property entailed or necessarily entailed by a rational/consistent property is rational/consistent.
T2 Maximal-rationality is a rational/consistent property.
It follows: A maximally-rational entity necessarily exists.
It would still be possible, but not mandatory, to understand a maximally-rational being also as a Godlike being.
Independent of this discussion we expect the Isabelle/HOL theory files we contributed to be useful for teaching quantified modal logics in classroom, as previously demonstrated by Wisniewski et al. (2016) in their awarded lecture course on “Computational Metaphysics”. The developed corpus of example problems is furthermore suited as a benchmark for other ambitious knowledge representation and reasoning projects in the KR community: Can the alternative approaches encode such metaphysical argumants as well? How about their proof automation capabilities and how about model finding? For example, description logic or argumentation theory, due to their limited expressivity, appear unsuited to support such ambitious applications, while the techniques presented in this paper have meanwhile been used successfully for the encoding and assessment of foundational theories in metaphysics (Kirchner, Benzm¨uller, and Zalta 2020) and mathematics (Benzm¨uller and Scott 2020; Tiemens et al. 2020). Moreover, our problem set constitutes an interesting benchmark for other HOL automated theorem provers and should therefore be converted into TPTP THF (Sutcliffe and Benzm¨uller 2010) representation and be used in theorem prover competitions.
G¨odel’s modal ontological argument stands in prominent tradition of western philosophy. It has its roots in the Proslogion of Anselm of Canterbury and it has been picked up in Descartes’ Fifth Meditation and in the works of Leibniz, which in turn inspired and informed the work of G¨odel.
In this paper we have linked G¨odel’s theory to a suitably adapted mathematical theory (modal filter and modal ultrafilter), and subsequently we have developed simplified modal ontological arguments which avoid some of G¨odel’s axioms and consequences, including modal collapse, that have led to criticism in the past. At the same time the offered simplifications are very far reaching, eventually too far. Anyhow, the insights that were presented in this paper appear relevant to inform ongoing studies of the modal ontological argument in theoretical philosophy and theology.
We have in this paper applied modern symbolic AI techniques to arrive at deep, explainable and verifiable models of the metaphysical concepts we are interested in. In particular, we have illustrated how state of the art theorem proving systems, in combination with latest knowledge representation and reasoning technology, can fruitfully be employed to explore and contribute deep new knowledge to other disciplines.
I am grateful to friends and colleagues who have supported this line of research in the past and/or directly contributed with comments and suggestions, including (in alphabetical order) C. Brown, M. Droste, D. Fuenmayor, T. Gleißner, D. Kirchner, S. Kovaˇc, T. Lethen, X. Parent, R. Rojas, D. Scott, A. Steen, L. van der Torre, E. Weydert, D. Streit, B. Woltzenlogel-Paleo, E. Zalta. Moreover, I am grateful to the reviewers of this paper for useful comments and for the pointer to P. Odifreddi’s paper.
Alama, J.; Oppenheimer, P. E.; and Zalta, E. N. 2015. Automating leibniz’s theory of concepts. In Automated Deduction – CADE-25, volume 9195 of LNCS, 73–97. Springer.
Anderson, C. A., and Gettings, M. 1996. G¨odel’s ontological proof revisited. In G¨odel’96: Logical Foundations of Mathematics, Computer Science, and Physics: Lecture Notes in Logic 6. Springer. 167–172.
Anderson, C. A. 1990. Some emendations of G¨odel’s ontological proof. Faith and Philosophy 7(3):291–303.
Andrews, P. B. 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, volume 27 of Applied Logic Series. Springer.
Benzm¨uller, C., and Andrews, P. 2019. Church’s type theory. In Zalta, E. N., ed., The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, summer 2019 edition. Benzm¨uller, C., and Fuenmayor, D. 2020. Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of G¨odel’s ontological argument. Bulletin of the Section of Logic. To appear, preprint: https://arxiv.org/abs/1910.08955.
Benzm¨uller, C., and Paulson, L. 2013. Quantified multimodal logics in simple type theory. Logica Universalis 7(1):7–20.
Benzm¨uller, C., and Scott, D. S. 2020. Automating free logic in HOL, with an experimental application in category theory. Journal of Automated Reasoning 64(1):53–72.
Benzm¨uller, C., and Woltzenlogel Paleo, B. 2014. Automating G¨odel’s ontological proof of God’s existence with higher-order automated theorem provers. In ECAI 2014, volume 263 of Frontiers in Artificial Intelligence and Applications, 93–98. IOS Press.
Benzm¨uller, C., and Woltzenlogel Paleo, B. 2016. The inconsis- tency in G¨odel’s ontological argument: A success story for AI in metaphysics. In Kambhampati, S., ed., IJCAI 2016, volume 1-3, 936–942. AAAI Press.
Benzm¨uller, C. 2019. Universal (meta-)logical reasoning: Recent successes. Science of Computer Programming 172:48–62.
Blanchette, J. C., and Nipkow, T. 2010. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Kaufmann, M., and Paulson, L. C., eds., Interactive Theorem Proving — ITP 2010, volume 6172 of LNCS, 131–146. Springer.
Blumson, B. 2017. Anselm’s God in Isabelle/HOL. Archive of Formal Proofs.
Burris, S., and Sankappanavar, H. 1981. A Course in Universal Algebra. Springer.
Fitelson, B., and Zalta, E. N. 2007. Steps toward a computational metaphysics. Journal Philosophical Logic 36(2):227–247.
Fitting, M. 2002. Types, Tableaus, and G¨odel’s God. Kluwer.
Fuenmayor, D., and Benzm¨uller, C. 2017. Automating emenda- tions of the ontological argument in intensional higher-order modal
logic. In KI 2017: Advances in Artificial Intelligence, volume 10505 of LNAI, 114–127. Springer.
Garson, J. 2018. Modal logic. In Zalta, E. N., ed., The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, fall 2018 edition.
G¨odel, K. 1970. Appendix A. Notes in Kurt G¨odel’s Hand. In Sobel (2004). 144–145.
Kanckos, A., and Lethen, T. 2019. The development of G¨odel’s ontological proof. The Review of Symbolic Logic.
Kanckos, A., and Paleo, B. W. 2017. Variants of G¨odel’s ontolog- ical proof in a natural deduction calculus. Studia Logica 105:553– 586.
Kirchner, D.; Benzm¨uller, C.; and Zalta, E. N. 2019. Computer science and metaphysics: A cross-fertilization. Open Philosophy 2:230–251.
Kirchner, D.; Benzm¨uller, C.; and Zalta, E. N. 2020. Mechanizing principia logico-metaphysica in functional type theory. Review of Symbolic Logic 13(1):206–218.
Kovaˇc, S. 2012. Modal collapse in G¨odel’s ontological proof. In Szatkowski, M., ed., Ontological Proofs Today. Ontos Verlag. 50– 323.
Nipkow, T.; Paulson, L. C.; and Wenzel, M. 2002. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer.
Odifreddi, P. 2000. Ultrafilters, dictators, and gods. In Calude, C., and Paun, G., eds., Finite Versus Infinite. Discrete Mathematics and Theoretical Computer Science. Springer, London. 239–245.
Oppenheimer, P. E., and Zalta, E. N. 1991. On the logic of the ontological argument. Philosophical Perspectives 5:509–529.
Oppenheimer, P. E., and Zalta, E. N. 2011. A computationally- discovered simplification of the ontological argument. Australasian Journal of Philosophy 89(2):333–349.
Pelletier, F. J., and Zalta, E. N. 2000. How to Say Goodbye to the Third Man. Noˆus 34(2):165–202.
Rushby, J. 2018. A mechanically assisted examination of begging the question in Anselm’s ontological argument. J. Applied Logics 5(7):1473–1496.
Scott, D. S. 1972. Appendix B: Notes in Dana Scott’s Hand. In Sobel (2004). 145–146.
Sobel, J. H. 1987. G¨odel’s ontological proof. In Tomson, J. J., ed., On Being and Saying. Essays for Richard Cartwright. MIT Press. 241–261.
Sobel, J. H. 2004. Logic and Theism: Arguments for and Against Beliefs in God. Cambridge University Press.
Sutcliffe, G., and Benzm¨uller, C. 2010. Automated reasoning in higher-order logic using the TPTP THF infrastructure. Journal of Formalized Reasoning 3(1):1–27.
Tiemens, L.; Scott, D. S.; Benzm¨uller, C.; and Benda, M. 2020. Computer-supported exploration of a categorical axiomatization of modeloids. In Relational and Algebraic Methods in Computer Science – 18th International Conference, RAMiCS 2020, volume 12062 of LNCS, 302–317. Springer.
Wisniewski, M.; Steen, A.; and Benzm¨uller, C. 2016. Einsatz von Theorembeweisern in der Lehre. In Schwill, A., and Lucke, U., eds., Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik, Commentarii informaticae didacticae (CID), 81–92. Universit¨atsverlag Potsdam.
Zalta, E. N. 1993. Twenty-Five Basic Theorems in Situation and World Theory. Journal of Philosophical Logic 22(4):385–428.
Figure 11: Formal study of “version No.2” of G¨odel’s argument as reported by Kanckos and Lethen (2019).