Gödel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF

Christoph Benzmüller

cs.LOSep 14, 2026

Gödel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF

Authors: Christoph Benzmüller

Organizations: AI Systems Engineering, Otto-Friedrich-Universität Bamberg, Germany · Faculty of Mathematics and Computer Science, Freie Universität Berlin, Germany

Abstract

The Isabelle/HOL dataset of Benzmüller and Scott's study of Gödel's ontological argument and Scott's variant (Monatshefte für Mathematik, 2025) is carried to Lean 4 and from there back to the automated provers, as a benchmark independent of either proof assistant. The port covers all thirty theories, structure and names preserved: 548 statements compare identical as parsed, every named result is proved again, and five results the original reports without replaying them are proved here. For every theorem, #print axioms gives the postulates its proof consumes: Scott's necessary existence and modal collapse need only a symmetric frame, confirming that KB suffices. The benchmark, in TPTP THF and SMT-LIB, turns the steps of an argument debated in philosophy into 294 theorems, alongside 45 statements the original refutes or leaves open, ten left open there. Five THF provers, and cvc5 on SMT-LIB, prove 227 theorems within ten seconds on one core and 232 within sixty, and none proves any of the 45. E and Leo-II solve the most, although Leo-II's calculus has been unchanged for about a decade and was only repaired and modernised here, as release 2.2. Vampire, whose later version won the higher-order division of CASC-30, solves the most in no configuration. Only E and Leo-II are measured in their own automatic mode: Zipperposition proves 101 in a single mode and 213 with its developers' portfolio, Vampire 174 without options and 209 with a higher-order schedule that its CASC mode does not select, and Leo-III 159 alone and 177 with E as partner.

Figures & tables

Isabelle/HOL	Lean 4	Isabelle/HOL	Lean 4	Isabelle/HOL	Lean 4	Isabelle/HOL	Lean 4
$\bot$	$\bot$ m	$\top$	$\top$ m	$\forall$	$\forall$ m	$\exists$	$\exists$ m
$\neg$	$\neg$ m	$\wedge$	$\wedge$ m	$\forall^{E}$	$\forall$ E	$\exists^{E}$	$\exists$ E
$\vee$	$\vee$ m	$\supset$	$\rightarrow$ m	$\leftrightarrow$	$\leftrightarrow$ m	$\mathbf{r}$	$\mathsf{r}$
$\Box$	$\Box$	$\Diamond$	$\Diamond$	$=$	$=$ m	$\neq$	$\neq$ m
$\equiv$	$\equiv$ m	$\lfloor\cdot\rfloor$	$\lfloor\cdot\rfloor$	$\supset_{N}$	$\supset$ N	$@$	$@$ m

Table 1: Notation of the Isabelle/HOL sources and of the Lean 4 port.

Isabelle/HOL	Lean 4
typedecl i , typedecl e	axiom i : Type , axiom e : Type (with Nonempty )
type_synonym	abbrev
consts , axiomatization where	axiom (free variables become explicit binders)
abbreviation (unfolded at parse time)	@[simp, grind] def (unfolded by simp / grind )
definition f with f_def	def f , unfolded definitionally or by simp [f]
lemma … oops after nitpick	example … := by countermodel

Table 2: Correspondence of Isabelle/HOL and Lean 4 constructions.

	total	prose	declarations	proof
Isabelle/HOL (30 theories)	1157	180	765	212
Lean 4 (30 modules)	1868	517	854	497

Table 3: Non-blank lines of source by kind. A one-line statement with an inline proof ( by blast , := term ) counts as one declaration line on either side; only lines of proof below the statement count as proof. Declarations include notation and module headers.

Module	Result	Frame conditions	Other postulates used
GoedelVariantHOML1	Inconsistency	—	Ax2a Ax3 Ax4 iNonempty
GoedelVariantHOML1inS4	Th3	Rrefl	Ax3
GoedelVariantHOML2	Th1	—	Ax2a Ax2b
GoedelVariantHOML2	Th4	—	Ax1Gen Ax2a
GoedelVariantHOML2	Th5 , MC	Rsymm	Ax1Gen Ax2a Ax2b Ax3
GoedelVariantHOML2	Monotheism	—	Ax2a

Table 4: Postulates consumed by the proofs of the principal theorems, as reported by #print axioms ; upper bounds for what the theorems require. Omitted are only the three standard Lean 4 axioms ( propext , Classical.choice , Quot.sound ) and the embedding’s signature constants ( i , e , R , existsAt , P ); everything else a proof depends on is listed, including the non-emptiness postulates iNonempty . The possibilist and mixed-quantifier variants agree with the entries of their actualist counterparts except where a row of their own is shown ( GoedelVariantHOML2AndersonQuant , Section 5 ).

prover	configuration	10 s	60 s	machine	alone
E 3.2.5-ho	--auto-schedule	218	220	227	8
	--auto	209	212	–
Leo-II 2.2	with first-order E	218	221	226	1
Vampire 4.8 HO	snake_tptp_hol	209	219	218	0
	no options	174	174	–
	--mode casc	167	186	185

Table 5: The 294 THF problems at 10 and at 60 seconds on one core and on the whole machine, against the four higher-order provers Isabelle2025-2 bundles, E [ 33 ] , Vampire [ 22 ] , Zipperposition [ 4 ] and cvc5 [ 2 ] , and against Leo-II [ 17 , 7 ] and Leo-III [ 36 ] ; the versions are in the rows. Each prover’s first row is its recommended configuration (Section 6.2 ), the rows beneath it are further configurations, named by their options; a dash marks a column a configuration does not have. Provers are ordered by their first rows, summed over the three columns. “Alone” counts the problems a prover proves in its first row at 10 seconds that no other first row proves; the last row is the union of the first rows, with the one-core figures of Leo-III and cvc5 in the machine column. cvc5 runs on the SMT-LIB rendering of the same statements.

stratum	problems	E	Leo-II	Vampire	Leo-III
a variable applied to a lambda	872	510	214	265	203
no such application	2765	1907	1675	1539	1428
100 formulas or more	1033	614	282	318	174
fewer than 100	2604	1803	1607	1486	1457
the profile of these problems	438	267	262	207	193
these problems	294	218	218	174	159

Table 6: The 3637 monomorphic TH0 problems of TPTP v7.5.0 by stratum, at ten seconds on one core, in the versions of Table 5 but with Vampire without options and Leo-III without E, and the same figures for the problems of this paper, which are those of the corresponding rows of Table 5 . The profile is: a lambda somewhere, no variable applied to a lambda, no Boolean argument, highest type order three, between 50 and 100 formulas. Zipperposition and cvc5 were not run over the library.

Explore similar work

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes
Sep 28, 2026Christoph BenzmüllerFirst-Order Logic Axiom
AI Systems Engineering, Otto-Friedrich-Universität Bamberg, Germany · Faculty of Mathematics and Computer Science, Freie Universität Berlin, Germany
Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement
Jun 4, 2026Jui-Hui Chung, Ziyang Cai, Zihao Li +14Theorem Proving Agentic Framework
1Princeton Language and Intelligence, Princeton University · 2Amazon.
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
May 26, 2026Jinzheng Li, Zeru Zhu, Yuanjie RenTheorem Proving
1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

Sep 28, 2026, cs.LOJ/K move · Enter open · S save

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Christoph Benzmüller

AI Systems Engineering, Otto-Friedrich-Universität Bamberg, Germany · Faculty of Mathematics and Computer Science, Freie Universität Berlin, Germany

First-Order Logic Axiom Proof Ontology Counter Turing Test Modalities

Open paper AskPDF arXiv

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument (2025), reaches beyond the modal object language of the arguments: its property quantifiers range over terms that may also express nominals and satisfaction operators of hybrid logic, and a proof using one proves a theorem of the embedding that need not be one of the modal logic. That the framework affords this is not new, and whether a result is one of the modal logic can be settled in two ways: by replaying it in an explicit proof calculus, done by hand for chosen theorems, or by analysing the proofs the embedding itself produces, done here mechanically, for every result at once. Every statement the Notes prove has a proof inside the object language: 294 written out by hand and machine-checked, none using a nominal. The proofs the Notes themselves give instantiate no nominal either; what the detector flags there are terms a prover substituted. The three questions the Notes leave open are settled too, without nominals, but the conjunction axiom has to be emended: generalised in the Notes to Gödel's "any number of summands", it covers the conjunction of no properties, and of one; the empty one alone settles all three, and the two together yield what a separate axiom of Gödel's is for. This article restricts the conjunction axiom to at least two different conjuncts, the reading Gödel's footnote suggests, and the questions are settled again, by proofs that turn on the argument rather than a degenerate instance. The restriction holds of the object language only: with a nominal the axioms make the accessibility relation the identity and the readings coincide. Every theorem is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, certified by the build.

Abstract

Explore similar work

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving