论文标题
戈德尔本体论论点的简化变体
A Simplified Variant of Gödel's Ontological Argument
论文作者
论文摘要
提出了戈德尔本体论论点的简化变体。简化的参数已经在基本的模态逻辑K或KT中有效，它不会遭受模态崩溃，并且避免了Gödel所使用的相当复杂的本质（ESS。）和必要的存在（NE）的复杂谓词。提出的变体是作为与现代证明助手系统相互作用进行的一系列理论简化实验的结果。这些实验的起点是计算机编码Gödel的参数，然后系统地应用了自动推理技术以得出所呈现的简化变体。因此，提出的工作体现了计算形而上学中富有成果的人类计算机相互作用。所提出的结果是增加还是降低本体论论点的吸引力和说服力，这是我想将其传达给哲学和神学的问题。
A simplified variant of Gödel's ontological argument is presented. The simplified argument is valid already in basic modal logics K or KT, it does not suffer from modal collapse, and it avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel. The variant presented has been obtained as a side result of a series of theory simplification experiments conducted in interaction with a modern proof assistant system. The starting point for these experiments was the computer encoding of Gödel's argument, and then automated reasoning techniques were systematically applied to arrive at the simplified variant presented. The presented work thus exemplifies a fruitful human-computer interaction in computational metaphysics. Whether the presented result increases or decreases the attractiveness and persuasiveness of the ontological argument is a question I would like to pass on to philosophy and theology.
