A simplified variant of G\"odel'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\"odel. 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\"odel'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.
翻译:G\“odel”的肿瘤学论点的简化变式被提出来。简化的论据已经在基本模式逻辑K或KT中有效,它不会受到模式崩溃的影响,它避免了G\“odel”使用的相当复杂的精髓(Es.)和必要存在(NE)的前提。提出的变式是一系列与现代证据助理系统互动进行的理论简化实验的副结果。这些实验的出发点是计算机编码G\“odel”的论点,然后系统应用自动化推理技术来达成所提出的简化变式。因此,所提出的工作展示了计算元物理中的人类计算机之间富有成效的互动。所呈现的结果是增加还是降低本体学论点的吸引力和说服力,这是我想转而转而转而到哲学和理论学上的问题。