The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics

Abstract

This paper discusses the discovery of the inconsistency in Gödel's ontological argument as a success story for artificial intelligence. Despite the popularity of the argument since the appearance of Gödel's manuscript in the early 1970s, the inconsistency of the axioms used in the argument remained unnoticed until 2013, when it was detected automatically by the higher-order theorem prover Leo-II. Understanding and verifying the refutation generated by the prover turned out to be a time-consuming task. Its completion, as reported here, required the reconstruction of the refutation in the Isabelle proof assistant, and it also led to a novel and more efficient way of automating higher-order modal logic S5 with a universal accessibility relation. Furthermore, the development of an improved syntactical hiding for the utilized logic embedding technique allows the refutation to be presented in a human-friendly way, suitable for non experts in the technicalities of higher-order theorem proving. This brings us a step closer to wider adoption of logic-based artificial intelligence tools by philosophers.