Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Logic embeddings provide an elegant means to formalize sophisticated non-classical logics in classical higher-order logic (HOL, Church’s simple type theory [14]). In previous work (cf. [4] and the references therein) the embeddings approach has been successfully applied to automate object-level and meta-level reasoning for a range of logics and logic combinations with off-the-shelf HOL theorem provers. This also includes quantified modal logics (QML) [9] and quantified conditional logics (QCL) [3]. For many of the embedded logics few or no automated theorem provers did exist before. HOL is exploited in this approach to encode the semantics of the logics to be embedded, for example, Kripke semantics for QMLs [15] or selection function semantics for QCLs [26].

The embeddings approach is related to labelled deductive systems [18], which employ meta-level (world-)labeling techniques for the modeling and implementation of non-classical proof systems. In our embeddings approach such labels are instead encoded in the HOL logic.

The embedding approach is flexible, because various modal logics (even with multiple modalities or a mix of varying/cumulative domain quantifiers) can be easily supported by stating their characteristic axioms. Moreover, it is relatively simple to implement, because it does not require any modification in the source code of the higher-order prover. A minimal encoding of second-order modal logic KB in TPTP THF syntax [27] — this syntax is accepted by a range of HOL automated theorem provers (ATPs) — is exemplarily provided in Fig. 1.Footnote 1 The given set of axioms turns any TPTP THF compliant HOL-ATP in a reasoning tool for second-order modal logic. A Henkin-style semantics is thereby assumed for both logics: HOL and second-order modal logic.

Fig. 1.
figure 1

HOL encoding of second-order modal logic KB in THF syntax. Modal formulas are mapped to HOL predicates (with type $i>$o); type $i now stands for possible worlds. The modal connectives \(\lnot \) (mnot), \(\vee \) (mor) and \(\square \) (mbox), universal quantification for individuals (mall_ind) and for sets of individuals (mall_indset) are introduced in lines 7–18. Validity of lifted modal formulas is defined in the standard way (lines 20–21). Symmetry of accessibility relation r is postulated in lines 23–26. Hence, second-order KB is realized here; for logic K the symmetry axiom can be dropped.

Full size image

In recent work [5, 6, 8] we have applied the embedding approach to verify and automate a philosophical argument that has fascinated philosophers and theologians for about 1000 years: the ontological argument for the existence of God [25]. We have thereby concentrated on Gödel’s [19] modern version of this argument and on Scott’s [24] modification, which employ a second-order modal logic (S5) for which, until now, no theorem provers were available. In our computer-assisted study of the argument, the HOL provers LEO-II [10], Satallax [13] and Nitpick [12] have made some interesting observations, some of which were unknown so far. This is a landmark result, with media repercussion in a global scale, and yet it is only a glimpse of what can be achieved by combining computer science, philosophy and theology.

We briefly summarize some of these observations: Nitpick confirms that Scott’s axioms are consistent, while LEO-II and Satallax demonstrate that Gödel’s original, slightly different axioms are inconsistent. As far as we are aware, this is a new result. As experiments with LEO-II revealed, the problem lies in a subtle difference in the definitions of the predicate essence he essential properties of an entity) between Gödel and Scott. In recent papers on the ontological argument (see e.g. below), some authors speak of an oversight/flaw by Gödel, some silently replace Gödel’s definition without commenting and some simply stay with it. Moreover, instead of using modal logic S5, LEO-II and Satallax can prove the final theorem (that is, \(\square \exists x. G(x)\), necessarily there exists God) already for modal logic KB. This is highly relevant since some philosophers have criticized Gödel’s argument for the use of logic S5. Axiom B (symmetry), however, cannot be dropped, which in turn is confirmed by Nitpick. LEO-II and Satallax can also show that Gödel’s and Scott’s axioms imply what is called the modal collapse: \(\phi \supset \Box \phi \). This expresses that contingent truth implies necessary truth (which can even be interpreted as an argument against free will; cf. [25]) and is probably the most fundamental criticism put forward against Gödel’s and Scott’s versions of the argument. Other theorems that can be shown by LEO-II and Satallax include flawlessness of God and monotheism.

Ongoing and future work concentrates on the systematic study of Gödel’s and Scott’s proofs. We have also begun to study more recent variants of the argument [1, 2, 11, 16, 17, 20, 21], which claim to remedy some fundamental problems of Gödel’s and Scott’s proofs, especially the modal collapse [7]. One interesting and very encouraging observation from these studies is, that the argumentation granularity typical of these philosophy papers is already within reach of the capabilities of our higher-order automated theorem provers. This provides good evidence for the potential relevance of the embedding approach (not only) w.r.t. other similar applications in metaphysics.

The long-term goal is to methodically determine the range of logical parameters (e.g., constant vs. varying domains, rigid vs. non-rigid terms, logics KB vs. S4 vs. S5, etc.) under which the proposed variants of the modern ontological argument hold or fail.

There have been few related works [22, 23], and they have focused solely on the comparably simpler, original ontological argument by Anselm of Canterbury. These works do not achieve the close correspondence between the original formulations and the formal encodings that can be found in our approach and they also do not reach the same degree of proof automation.

Our work attests the maturity of contemporary interactive and automated deduction tools for HOL and demonstrates the elegance and practical relevance of the embeddings-based approach. Most importantly, our work opens new perspectives towards computational metaphysics.