arXiv:2609.26806v2 Announce Type: replace-cross
Abstract: This paper presents a complete, structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzm\"uller and Scott's study of G\"odel's ontological argument and Scott's variant: 30 modules, one per theory, retaining section structure, declaration order and names up to documented renamings; a comparison tool certifies the 548 statements identical as parsed. Every named result the original proves is proved again, from the inconsistency of G\"odel's 1970 axioms to modal collapse, monotheism and the ultrafilter property of positive properties. Five statements the original reports proved but does not replay are proved here. The 45 statements it refutes with Nitpick (35) or leaves open (10) are anonymous sorrys nothing depends on.
Lean 4 has neither a sledgehammer nor a model finder, so automated proofs become explicit proof terms and the 65 Nitpick invocations are documentation. #print axioms then lists, as Isabelle/HOL's thm_deps would, the postulates each proof consumes, hence an upper bound on the modal logic it needs: the proofs of Scott's necessary-existence theorem and of modal collapse consume only symmetry of the accessibility relation, so KB suffices; those of the essence and monotheism lemmas, of the possible existence of a God-like being (with one recorded exception) and of the 1970 inconsistency consume none.
The port also renders the dataset in TPTP THF, the format in which G\"odel's argument was first mechanised, and in SMT-LIB: a metaprogram prints the 294 theorems as problems. Six provers (E, Vampire, Zipperposition, cvc5, Leo-II, Leo-III) prove 227 of them within ten seconds on one core, 231 within sixty, and none of the 45 left unproved; Leo-II, repaired here and released as 2.2, is level with E at ten seconds. The development needs no library beyond Lean 4's core; sources, tools, cross-checks and both renderings are ancillary files.
Abstract: This paper presents a complete, structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzm\"uller and Scott's study of G\"odel's ontological argument and Scott's variant: 30 modules, one per theory, retaining section structure, declaration order and names up to documented renamings; a comparison tool certifies the 548 statements identical as parsed. Every named result the original proves is proved again, from the inconsistency of G\"odel's 1970 axioms to modal collapse, monotheism and the ultrafilter property of positive properties. Five statements the original reports proved but does not replay are proved here. The 45 statements it refutes with Nitpick (35) or leaves open (10) are anonymous sorrys nothing depends on.
Lean 4 has neither a sledgehammer nor a model finder, so automated proofs become explicit proof terms and the 65 Nitpick invocations are documentation. #print axioms then lists, as Isabelle/HOL's thm_deps would, the postulates each proof consumes, hence an upper bound on the modal logic it needs: the proofs of Scott's necessary-existence theorem and of modal collapse consume only symmetry of the accessibility relation, so KB suffices; those of the essence and monotheism lemmas, of the possible existence of a God-like being (with one recorded exception) and of the 1970 inconsistency consume none.
The port also renders the dataset in TPTP THF, the format in which G\"odel's argument was first mechanised, and in SMT-LIB: a metaprogram prints the 294 theorems as problems. Six provers (E, Vampire, Zipperposition, cvc5, Leo-II, Leo-III) prove 227 of them within ten seconds on one core, 231 within sixty, and none of the 45 left unproved; Leo-II, repaired here and released as 2.2, is level with E at ten seconds. The development needs no library beyond Lean 4's core; sources, tools, cross-checks and both renderings are ancillary files.
This article has been indexed from cs.AI updates on arXiv.org
Read the original article: