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.

翻译：本文提出了哥德尔本体论论证的一个简化变体。该简化论证在基本模态逻辑K或KT中即有效，不遭受模态坍塌问题，且避免了哥德尔所使用的本质属性和必然存在这类较为复杂的谓词。该变体是在与现代证明助手的交互过程中，通过一系列理论简化实验的副产品而获得的。这些实验的起点是将哥德尔论证进行计算机编码，继而系统性地应用自动推理技术，最终得到本文呈现的简化变体。因此，本研究工作体现了计算形而上学的领域中富有成效的人机交互。至于该结果是否会增强或削弱本体论论证的吸引力和说服力，我愿将此问题留给哲学与神学领域去评判。