Christoph Benzmüller

Gödel’s ontological proof for the existence of God – as an inference from the level of rational, logical structure to the level of being – was strongly influenced by Leibniz’s monadology, which is based on the Ur-Monade – God – conceived as absolutely infinite. Gödel defines God as the maximum of positive properties and he characterizes this maximum (of being) with his postulates implicitly as an ultrafilter structure. Using maximality as criterion we have compared the set of positive properties in Scott’s version of Gödel’s theistic theory with modified variants of it to see whether a maximum is still achieved, or not, and what effect this has on modal collapse. The motivation for these, typically weakened, variants of Gödel’s theistic theory has been to avoid modal collapse and the limited determinism associated with it, and to show that the necessary existence of God can still be proved with less strong axioms. A weakening of the maximality criterion of the ultrafilter structure imposed by Gödel’s (and Scott’s) postulates have thus been applied to the set of positive properties in order to allow for alternative models in which modal collapse does not hold. In these alternative models, however, the maximality criterion for the basic quantity of positive properties is abandoned, so that in them God as a “maximum” is not reached. We argue that this is contrary to Gödel’s intention, and that for his conception of God, maximality and absolute infinity are non-negotiable. What Gödel had in mind, as we argue here, was a holistic – absolutely infinite – view of the world, i.e. with modal collapse, but without limited determinism.

Higher-order logic HOL offers a very simple syntax and semantics for knowledge representation and reasoning in various particular domains, including in particular representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to HOL theorem provers able to parse TPTP, thereby making all such provers able to run on DHOL problems.

Deep and shallow embeddings of non-classical logics in classical higher-order logic have been explored, implemented, and used in various reasoning tools in recent years. This paper presents a method for the simultaneous deployment of deep and shallow embeddings of various degrees in classical higher-order logic. This enables flexible, interactive and automated theorem proving and counterexample finding at meta and object level, as well as automated faithfulness proofs between these logic embeddings. The method is beneficial for logic education, research and application and is illustrated here using a simple propositional modal logic. However, this approach is conceptual in nature and not limited to this simple logic context.