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

Abstract

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzm\"uller and Scott's Notes on G\"odel's and Scott's variants of the ontological argument, reaches beyond the modal object language: its quantifiers range over domains containing the nominals and satisfaction operators of hybrid logic. A proof using one proves a theorem of the embedding, not necessarily of the modal logic. Whether a result is one of the modal logic can be settled by replaying it in an explicit calculus, or, more cheaply and for all results at once, by analysing what the embedding's proofs substitute. Every statement the Notes prove has a proof in the embedding substituting nothing outside the object language, 294 of them explicit. The Notes'own proofs substitute none either; what it flags are terms a prover introduced. A soundness theorem over general models closed under the object language, and a sentence of that language the embedding proves but which fails in one of them, fix what the certificate says. The Notes'three open questions are settled too, without nominals, but by the empty instance of the conjunction axiom, too cheaply to convince. Generalised to G\"odel's"any number of summands", the axiom covers the empty conjunction and the singleton. This article restricts it to at least two different conjuncts, a non-degenerate reading of G\"odel's footnote, and settles them again without nominals. In effect only the empty conjunction is excluded; the singleton comes back with the other axioms. In one variant the restriction refutes the possible existence of a God-like being; the answers return, with no side condition, once the Notes'non-emptiness clause is confined to G\"odel's essence. Every theorem here is verified in Isabelle/HOL and independently in Lean 4, the separating model in its propositional part; the countermodels are Nitpick's, checked by the build.