arXiv发布Gödel本体论论证浅层嵌入研究v3

Benzmüller 与 Scott 关于 Gödel 本体论论证变体的笔记中，浅嵌入的证明可触及模态对象语言之外的名义词与满足算子。作者证明笔记中全部 294 条陈述均存在不使用名义词的显式机器检验证明，并据此解决了笔记遗留的三个开放问题。该结论在 Isabelle/HOL 与 Lean 4 中独立验证，反模型由 Nitpick 生成并经构建检查。

摘自 arXiv Artificial Intelligence

还没有足够的连续观测数据，暂不绘制趋势。