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 生成并经构建检查。
正文 · AI 翻译
摘要：在经典高阶逻辑中对高阶模态逻辑的浅层嵌入——用于 Benzmüller 和 Scott 的《关于 Gödel 和 Scott 本体论论证变体的笔记》——超出了模态对象语言的范围：其性质量词的范围涵盖了包含混合逻辑的 nominal 和满足算子的域。使用其中一个进行的证明证明的是该嵌入的一个定理，而不一定是模态逻辑的定理。该框架提供这一点并不新鲜。一个结果是否属于模态逻辑，可以通过在显式演算中逐一重放来判定。更廉价地，并且一次性针对所有结果，可以通过分析该嵌入的证明替换了什么来处理。笔记所证明的每个陈述在该嵌入中都有一个在对象语言之外不替换任何内容的证明：其中 294 个是显式证明，经过机器检查，没有一个使用 nominal。笔记自身的证明也没有替换任何内容；检查所标记的是证明器引入的项。
笔记留下的三个问题也得到了解决，不使用 nominal，而是通过合取公理的空实例，这太廉价而无法令人信服。正如笔记将其推广以涵盖 Gödel 的“任意数量的被加项”，该公理涵盖了空合取和单元素。本文将限制为至少两个不同的合取项，这是对 Gödel 脚注的一种非退化解读，并再次解决了这些问题，不使用 nominal。实际上，该限制只排除了空合取；单元素情形随其他公理一同回归。在三个变体之一中，该限制反驳了类似上帝的存在者的可能存在性；一旦笔记的非空性条款被限制在 Gödel 的本质之上，答案便无条件地回归。此处陈述的每个定理都在 Isabelle/HOL 中验证，并独立地在 Lean 4 中验证；反模型是 Nitpick 的，由构建检查。
| 评论： | 46 页。v3 新增：对合取公理的另外两种解读——刚性集合，以及同时采用两种限制——与所采用的那一种进行权衡；并表明 Gödel 1970 年的本质与修复后的本质不可相互定义。辅助内容：Isabelle/HOL 和 Lean 4 中的每个定理，16 个解读会话，构建检查的 78 次 Nitpick 搜索，两个检测器及其报告，七个审计会话 |
| 主题： | 计算机科学中的逻辑 (cs.LO)；人工智能 (cs.AI)；逻辑 (math.LO) |
| MSC 分类： | 03B45, 03B15, 03B35, 03A05 |
| ACM 分类： | F.4.1; I.2.3 |
| 引用为： | arXiv:2609.36279 [cs.LO] |
| （或 arXiv:2609.36279v3 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2609.36279 arXiv 颁发的 DOI，通过 DataCite |
提交历史
来自：Christoph Benzmüller [查看电子邮件]
[v1]
2026 年 9 月 28 日星期一 21:09:57 UTC（281 KB）
[v2]
2026 年 10 月 1 日星期四 16:36:23 UTC（293 KB）
[v3]
2026 年 10 月 13 日星期二 17:47:40 UTC（444 KB）
来源：arXiv cs.AI · arxiv.org