哥德尔本体论论证的一个简化变体

本文给出了哥德尔本体论论证的一个简化变体。该简化论证在基本模态逻辑 K 或 KT 中即有效，它不受模态坍缩之苦，且避免了哥德尔所用的较为复杂的本质（Ess.）与必然存在（NE）谓词。所给出的变体是作者与现代证明辅助系统交互进行一系列理论简化实验的副产物。这些实验的起点是哥德尔论证的计算机编码，随后系统地应用自动化推理技术，从而得到所呈现的简化变体。因此，本文工作例证了计算形而上学中富有成果的人机交互。所呈现的结果究竟增强还是削弱了本体论论证的吸引力与说服力，我将此问题交由哲学与神学来回答。