Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Christoph Benzmüller

cs.LOSep 28, 2026

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Authors: Christoph Benzmüller

Organizations: AI Systems Engineering, Otto-Friedrich-Universität Bamberg, Germany · Faculty of Mathematics and Computer Science, Freie Universität Berlin, Germany

Abstract

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nominals and satisfaction operators of hybrid logic, and a proof using one proves a theorem of the embedding that need not be one of the modal logic. That the framework affords this is not new, and whether a result is one of the modal logic can be settled in two ways: by replaying it in an explicit proof calculus, done by hand for chosen theorems, or by analysing the proofs the embedding itself produces, done here mechanically, for every result at once. Every statement the Notes prove has a proof inside the object language: 294 written out by hand and machine-checked, none using a nominal. The proofs the Notes themselves give instantiate no nominal either; what the detector flags there are terms a prover substituted. The three questions the Notes leave open are settled too, without nominals, but the conjunction axiom has to be emended: generalised in the Notes to Gödel's "any number of summands", it covers the conjunction of no properties, and of one; the empty one alone settles all three, and the two together yield what a separate axiom of Gödel's is for. This article restricts the conjunction axiom to at least two different conjuncts, the reading Gödel's footnote suggests, and the questions are settled again, by proofs that turn on the argument rather than a degenerate instance. The restriction holds of the object language only: with a nominal the axioms make the accessibility relation the identity and the readings coincide. Every theorem is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, certified by the build.

Figures & tables

$\displaystyle\varphi\supset_{P}\psi$	$\displaystyle=\Box(\forall^{E}y.\ \varphi y\supset\psi y)$	plain inclusion
$\displaystyle\varphi\supset_{N}\psi$	$\displaystyle=\Box\bigl(\varphi\neq(\lambda x.\bot)\wedge\forall^{E}y.\ \varphi y\supset\psi y\bigr)$	inclusion of Fig. 8
$\displaystyle G\,x$	$\displaystyle=\forall\varphi.\ \mathcal{P}\varphi\supset\varphi x$	God-like
$\displaystyle\varphi\mathrel{\mathit{Ess}}x$	$\displaystyle=\forall\psi.\ \psi x\supset(\varphi\supset_{N}\psi)$	essence, Gödel’s own
$\displaystyle E\,x$	$\displaystyle=\forall\varphi.\ \varphi\mathrel{\mathit{Ess}}x\supset\Box\exists^{E}y.\ \varphi y$	necessary existence

Table 1

	variant 2	variant 3	Scott + 1Gen	hybrid?
G_ex	1Gen 2a 4	1Gen 2a 4	1Gen A1 A2	no
Th3 / T3	1Gen 2a 4	1Gen 2a 4 §	1Gen A1 A2	no
Th5	1Gen 2a 4	1Gen 2a 4 §	—	no
MC	1Gen 2a 2b 4	1Gen 2a 2b 4 §	1Gen A1 A2 A4	no
UniqueEss3	none	—	—	no
UniqueEss3_K	—	none	—	no

Table 1 : Postulates used by the Lean 4 proofs, as reported by #print axioms , and the verdict of the hybrid-witness detector. Axiom names drop their Ax prefix; signature constants, the non-emptiness of

e

and Lean 4 ’s three standard axioms are omitted. Rrefl is reflexivity. A hypothesis rather than an axiom is marked: ∗ that every world has an actual individual, † the side condition of Theorem 15 . § In variant 3 these are Th3_K , Th5_K and MC_K (Section 5 ). Blocks, from the top: the answers to the three open questions; their possibilist and mixed-quantifier copies (Section 5 ); the collapse results, which need nominals; the K -proofs of Section 7 , mixed setting of variant 2; the answers under Ax1GenTwo (Section 6.1 ); variant 3 with the non-emptiness clause confined to the essence (Section 6.2 ), where Th4 is a theorem.

Explore similar work

Jul 12, 2026cs.AI

First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness (Extended Preprint)

We extend, in Isabelle/HOL, the deep-and-shallow embedding methodology of our prior work from propositional to first-order modal logic (FML) with constant-domain Kripke semantics. Three embeddings of FML into classical higher-order logic (HOL) are provided side by side: a deep embedding, a heavyweight maximal-shallow embedding, and a lightweight minimal-shallow embedding. The minimal-shallow embedding is presented as an Isabelle/HOL locale, parametrised by an accessibility relation, a world-indexed interpretation, a universe of worlds, and a variable assignment; the locale form admits a global faithfulness theorem, stating that quantifying over all minimal-shallow interpretations recovers exactly deep validity. A central technical contribution is a mechanisation, for FML under constant-domain Kripke semantics, of the (countable) downward Löwenheim-Skolem theorem, which underpins the automation of our faithfulness proof between the deep and minimal-shallow embeddings. Deploying it inside an extension of the minimal-shallow locale resolves the surjectivity problem that arises against an uncountable domain of individuals -- where the locale's variable assignment, having countable domain V = nat, cannot be surjective onto the domain -- and thereby yields faithfulness over the full domain. Since prior work treats only the propositional fragment, we develop here the substitution machinery (free/bound-variable predicates, the fresh-variable function, capture-avoiding substitution, alphabetic renaming, the substitutability predicate, the substitution lemma, and size-based induction principles) needed for the first-order quantifiers.

Christoph Benzmüller, Daniel Kirchner

University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany

First-Order Logic Logic Theorem Proving

Ask PDF

Sep 14, 2026cs.LO

Gödel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF

The Isabelle/HOL dataset of Benzmüller and Scott's study of Gödel's ontological argument and Scott's variant (Monatshefte für Mathematik, 2025) is carried to Lean 4 and from there back to the automated provers, as a benchmark independent of either proof assistant. The port covers all thirty theories, structure and names preserved: 548 statements compare identical as parsed, every named result is proved again, and five results the original reports without replaying them are proved here. For every theorem, #print axioms gives the postulates its proof consumes: Scott's necessary existence and modal collapse need only a symmetric frame, confirming that KB suffices. The benchmark, in TPTP THF and SMT-LIB, turns the steps of an argument debated in philosophy into 294 theorems, alongside 45 statements the original refutes or leaves open, ten left open there. Five THF provers, and cvc5 on SMT-LIB, prove 227 theorems within ten seconds on one core and 232 within sixty, and none proves any of the 45. E and Leo-II solve the most, although Leo-II's calculus has been unchanged for about a decade and was only repaired and modernised here, as release 2.2. Vampire, whose later version won the higher-order division of CASC-30, solves the most in no configuration. Only E and Leo-II are measured in their own automatic mode: Zipperposition proves 101 in a single mode and 213 with its developers' portfolio, Vampire 174 without options and 209 with a higher-order schedule that its CASC mode does not select, and Leo-III 159 alone and 177 with E as partner.

Christoph Benzmüller

AI Systems Engineering, Otto-Friedrich-Universität Bamberg, Germany · Faculty of Mathematics and Computer Science, Freie Universität Berlin, Germany

Theorem Proving Proof Ontology Counter Turing Test

Ask PDF

Sep 7, 2026cs.LO

Monadic Second-Order Logic in HOL: Deep and Shallow with Automated Faithfulness (Extended Preprint)

In Isabelle/HOL, we apply the deep-and-shallow embedding methodology of our prior work to monadic second-order logic (MSO). Three embeddings are developed side by side: a deep embedding (an inductive datatype with an explicit satisfaction relation); a maximal-shallow embedding that translates the connectives and quantifiers directly into HOL, carrying the interpretation and both assignments explicitly; and a minimal-shallow embedding -- a locale that fixes those parameters, collapsing the formula type to bool. The enabling new ingredient is a two-sorted substitution apparatus -- capture-avoiding substitution, renaming, and a substitution lemma per namespace -- in which each binder is transparent for the other; faithfulness of all three embeddings is mechanised and largely automated. Our central contribution is a fully mechanised two-sorted downward Loewenheim-Skolem theorem: the minimal embedding recovers deep validity relative to the (countable) assignment ranges, and this range-relative reading is shown to coincide with the general (Henkin-style) reading of MSO, whereas the standard reading validates strictly more formulas, witnessed by comprehension. Both readings are nonetheless recovered from the minimal embedding, differing only in the admitted interpretations: all of them for the general reading, only the elementary substructures of the full model for the standard. We exercise the embeddings on classical MSO landmarks: the Boolean-closure and graph schemata hold under the full second-order domain yet fail in the minimal embedding, making the dichotomy concrete, while reachability and 2-colorability are refuted throughout.

Christoph Benzmueller, Daniel Kirchner

University of Bamberg, Bamberg, Germany · Freie Universität Berlin, Berlin, Germany

First-Order Logic Theorem Proving Induction

Ask PDF