Event Detail

I will report on the discovery and verification of the inconsistency in Gödel’s ontological argument with reasoning tools for higher-order logic. Despite the popularity of the argument since the appearance of Gödel’s manuscript in the early 70’s, 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 LEO-II turned out to be a time-consuming task. Its completion required the reconstruction of the refutation in the Isabelle/HOL proof assistant. This effort also led to a more efficient way of automating higher-order modal logic S5 with a universal accessibility relation within the logic embedding technique we utilize in our work.

The development of an improved syntactical hiding for the 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 should bring us a step closer to wider adoption of logic-based artificial intelligence tools by philosophers.

If time permits, I will also point to alternative, ongoing applications of the logic embeddings technique, such as the encoding of Zalta’s theory of abstract objects or the mechanization of Scott’s free logic.