arXiv Artificial Intelligence· Christoph Benzm\"uller·· 19 小时前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 生成并经构建检查。
来源：arXiv Artificial Intelligence · arxiv.org