arXiv cs.AI· Christoph Benzm\"uller·· 3 天前AI 评分12
无需名义词的本体论论证证明：Gödel 本体论论证的浅层嵌入与 Monatshefte 笔记未解问题
Proofs Without Nominals: G\"odel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
AI 导读
研究证明 Benzmüller 与 Scott 关于 Gödel 本体论论证的浅层嵌入中，294 条显式证明均未使用混合逻辑的名义词或满足算子，全部经机器验证。文章还以非退化方式限制合取公理，重新解决了笔记遗留的三个开放问题，其中一个变体下该限制反驳了上帝类存在者的可能存在。所有定理均在 Isabelle/HOL 与 Lean 4 中独立验证，反模型由 Nitpick 生成并经构建检查。
正文 · 原文
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, reaches beyond the modal object language: its property 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. That the framework affords this is not new. Whether a result is one of the modal logic can be settled by replaying it in an explicit calculus, one result at a time. More cheaply, and for all results at once, it can be approached 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 proofs, machine-checked, none using a nominal. The Notes' own proofs substitute none either; what the check flags are terms a prover introduced.
The three questions the Notes leave open are settled too, without nominals, but by the empty instance of the conjunction axiom, too cheaply to convince. As the Notes generalise it, to cover 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 the questions again, without nominals. In effect the restriction excludes only the empty conjunction; the one-element case comes back with the other axioms. In one of the three variants 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 stated here is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, checked by the build.
| Comments: | 46 pages. New in v3: two further readings of the conjunction axiom -- rigid sets, and both restrictions at once -- weighed beside the one adopted; and Goedel's essence of 1970 shown not interdefinable with the repaired one. Ancillary: every theorem in Isabelle/HOL and Lean 4, 16 sessions for the readings, 78 Nitpick searches the build checks, both detectors with reports, seven audit sessions |
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Logic (math.LO) |
| MSC classes: | 03B45, 03B15, 03B35, 03A05 |
| ACM classes: | F.4.1; I.2.3 |
| Cite as: | arXiv:2609.36279 [cs.LO] |
| (or arXiv:2609.36279v3 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2609.36279 arXiv-issued DOI via DataCite |
Submission history
From: Christoph Benzmüller [view email]
[v1]
Mon, 28 Sep 2026 21:09:57 UTC (281 KB)
[v2]
Thu, 1 Oct 2026 16:36:23 UTC (293 KB)
[v3]
Tue, 13 Oct 2026 17:47:40 UTC (444 KB)
来源：arXiv cs.AI · arxiv.org