Summary
Gödel’s ontological argument is a famous logical argument about the existence of God, using special logical systems. The authors look at a method that translates these modal logical arguments into classical logic, checking if the proofs really stay inside the intended logic or not. They show that all the proofs can be done without relying on certain complex elements called nominals, and they fix some assumptions about combining properties to better match Gödel’s original ideas. Their work confirms these proofs using two computer proof systems and clarifies open questions left in earlier studies.
What this means in practice
- •For formal verification engineers: Validate complex higher-order modal logic proofs within classical proof assistants to ensure rigor in system correctness proofs involving modal concepts.
- •For automated theorem proving developers: Improve theorem prover design by clarifying when modal logic proofs can avoid nominals, reducing complexity in proof search algorithms.
A theory result. No direct application yet.
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, which this article does 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, and 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.