Automating Gödel’s ontological proof of God’s existence with higher-order automated theorem provers. (English) Zbl 1366.03169

Benzmüller, Christoph; Woltzenlogel Paleo, Bruno

Schaub, Torsten (ed.) et al., ECAI 2014. 21st European conference on artificial intelligence, Prague, Czech Republic, August 18–22, 2014. Proceedings. Including proceedings of the accompanied concerence on prestigious applications of intelligent systems (PAIS 2014). Amsterdam: IOS Press (ISBN 978-1-61499-418-3/pbk; 978-1-61499-419-0/ebook). Frontiers in Artificial Intelligence and Applications 263, 93-98 (2014).

Summary: Kurt Gödel’s ontological argument for God’s existence has been formalized and automated on a computer with higher-order automated theorem provers. From Gödel’s premises, the computer proved: necessarily, there exists God. On the other hand, the theorem provers have also confirmed prominent criticism on Gödel’s ontological argument, and they found some new results about it.
The background theory of the work presented here offers a novel perspective towards a computational theoretical philosophy.
For the entire collection see [Zbl 1296.68011].

MSC:

03B35	Mechanization of proofs and logical operations
68T05	Learning and adaptive systems in artificial intelligence
03A05	Philosophical and critical aspects of logic and foundations

Software:

E Theorem Prover; Isabelle/HOL; LEO-II; Nitpick; Prover9; PVS; Satallax; TPTP