无名义词的证明：哥德尔本体论论证、其浅嵌入及《数学月刊》笔记中的开放问题
Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
浏览论文内容
中文总结 AI 辅助
本文通过机械分析浅嵌入证明，证实哥德尔本体论论证的294个定理均可在无名义词的对象语言内证明，并修正合取公理后解决了《数学月刊》笔记遗留的三个开放问题。
中文摘要 AI 辅助
高阶模态逻辑在经典高阶逻辑中的浅嵌入，被用于本茨米勒和斯科特关于哥德尔与斯科特本体论论证变体的笔记（2025年），其能力超出了论证的模态对象语言：其性质量词所作用的项还可表达混合逻辑的名义词与满足算子，而使用名义词的证明所证明的是嵌入的一个定理，该定理未必是模态逻辑的定理。该框架具备此能力并非新发现，而一个结果是否属于模态逻辑可通过两种方式判定：在显式证明演算中重放该证明（对选定定理手工进行），或分析嵌入本身所产生的证明——本文对所有结果一次性机械地执行了后者。笔记所证的每个命题在对象语言内均有证明：294个证明由手工写出并经机器检验，无一使用名义词。笔记自身给出的证明也未实例化任何名义词；检测器所标记的只是证明器替换的项。笔记遗留的三个问题亦已解决，且无需名义词，但合取公理须加以修正：笔记中将其推广为哥德尔的“任意多个加项”形式，该形式涵盖零个性质与一个性质的合取；仅空合取即可解决全部三个问题，而两者结合则产生哥德尔单独公理所对应的结果。本文将合取公理限制为至少两个不同合取项，即哥德尔脚注所暗示的读法，并再次通过依赖于论证本身而非退化实例的证明解决了这些问题。该限制仅适用于对象语言：若引入名义词，公理将使可达关系成为同一关系，两种读法遂重合。每个定理均在Isabelle/HOL中验证，并在Lean 4中独立验证；反模型由Nitpick生成，并经构建过程认证。
英文摘要
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 (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nominals and satisfaction operators of hybrid logic, and a proof using one proves a theorem of the embedding that need not be one of the modal logic. That the framework affords this is not new, and whether a result is one of the modal logic can be settled in two ways: by replaying it in an explicit proof calculus, done by hand for chosen theorems, or by analysing the proofs the embedding itself produces, done here mechanically, for every result at once. Every statement the Notes prove has a proof inside the object language: 294 written out by hand and machine-checked, none using a nominal. The proofs the Notes themselves give instantiate no nominal either; what the detector flags there are terms a prover substituted. The three questions the Notes leave open are settled too, without nominals, but the conjunction axiom has to be emended: generalised in the Notes to Gödel's "any number of summands", it covers the conjunction of no properties, and of one; the empty one alone settles all three, and the two together yield what a separate axiom of Gödel's is for. This article restricts the conjunction axiom to at least two different conjuncts, the reading Gödel's footnote suggests, and the questions are settled again, by proofs that turn on the argument rather than a degenerate instance. The restriction holds of the object language only: with a nominal the axioms make the accessibility relation the identity and the readings coincide. Every theorem is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, certified by the build.
发表机构
- Otto-Friedrich-Universität Bamberg（班贝格奥托-弗里德里希大学）
- Freie Universität Berlin（柏林自由大学）
机构由 AI 辅助整理，请以论文原文为准。
