arXiv:2609.36279 · v5
Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
摘要
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 such a model, 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 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ödel'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ödel'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.
作者备注：51 pages. New in v5: the witness criterion and the whole-term condition come apart (a proof with the nominal in a context alone); three open questions answered by Bjoern Lindheim's harness, cited; both detectors read schema positions off the rule, the Isabelle/HOL one every rule, with a whole-term mode; 114 facts of the Notes replayed in Isar. Ancillary: sources, sessions, detectors, reports