A Simplified Variant of Gödel’s Ontological Argument

要約

G\’odel の存在論的議論の簡略化された変形が提示されます。
簡略化された引数は、基本的な様相論理 K または KT ですでに有効であり、様相崩壊に悩まされることはなく、G\’odel で使用される本質 (Ess.) と必要存在 (NE) のかなり複雑な述語を回避します。
提示されたバリアントは、最新の証明アシスタント システムとの相互作用で行われた一連の理論単純化実験の副次的結果として得られました。
これらの実験の出発点は、G\’odel の議論のコンピューター エンコードであり、その後、自動推論技術が体系的に適用されて、提示された簡略化されたバリアントに到達しました。
したがって、提示された研究は、計算形而上学における人間とコンピューターの実りある相互作用を例示しています。
提示された結果が存在論的議論の魅力や説得力を増加させるか減少させるかは、私が哲学と神学に伝えたい問題です。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google