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

Christoph Benzmüller

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, 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ödel's "any…