arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2609.26806

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

Christoph Benzmüller
View original source ↗Read source document ↗Export metadata ↓

Abstract

This paper presents a complete, structure-preserving port to Lean 4 of the Isabelle/HOL dataset accompanying Benzmüller and Scott's study of Gödel's modal ontological argument and Scott's variant of it. The port comprises 30 Lean 4 modules, one per Isabelle/HOL theory, retaining the section structure, the declaration order and the name of every axiom, definition, lemma and theorem; a comparison tool certifies all 548 statements identical. Everything the Isabelle/HOL development proves is proved again, including the inconsistency of Gödel's 1970 axioms, the repaired Gödel variants, Scott's variant, modal collapse, monotheism and the ultrafilter property of the positive properties; five statements the original leaves unreplayed after an automated prover had found a proof, one of which it then postulates, are proved as well. The 45 remaining unproved statements are exactly those the original refutes by nitpick (35) or leaves open (10); they are anonymous sorrys on which nothing depends. Two features of Lean 4 shape the result. It has neither a sledgehammer nor a model finder, so the one-line automated proofs become explicit proof terms and the 72 nitpick invocations are recorded as documentation. And #print axioms reports the postulates each proof consumes, giving for every result an upper bound on the modal logic it requires: Scott's necessary-existence theorem and modal collapse need only symmetry of the accessibility relation (logic KB); the essence and monotheism lemmas and the possible existence of a God-like being need no frame condition (the latter with the one exception the original records, the mixed-quantifier setting); and the inconsistency of Gödel's 1970 axioms needs none either. The development depends on no library beyond Lean 4's core; sources, comparison tools and two Isabelle cross-check sessions are included as ancillary files.

Explore related subjects

cs.LOcs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Christoph Benzmüller. 2026-09-14. Gödel's and Scott's Variants of the Ontological Argument in Lean 4. https://arxiv.org/abs/2609.26806

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Arithmetics within the Linear Time Hierarchy

We identify fragments of the arithmetic $S_1$ that enjoy nice closure properties and have exact characterization of their definable multifunctions. To do this, in the language of $S_1$, $L_1$, starting from the formula classes, $Σ^{\mathsf b}_{i}$, which ignore sharply bounded quantifiers when determining quantifier alternations, we define new syntactic classes by counting bounded existential sharply bounded universal quantifiers blocks. Using these, we define arithmetics: $\breve{S}^{i}_{1}$, $TLS^i_1$ and $TSC^i_1$. $\breve{S}^{i}_{1}$ consists of open axioms for the language symbols and length induction for one of our new classes, $SIUT_{i,1}^{\{p(|id|)\}}$. $TLS^i_1$ and $TSC^i_1$ are defined using axioms related to dependent choice sequences for formulas from two other classes within $Σ^{\mathsf b}_{i}$. We prove for $i \geq 1$ that $$TLS^i_1 \subseteq TSC^i_1 \subseteq \breve{S}^{i}_{1} \preceq_{\forall B(SITT_{i+1}^{\{p(|id|)\}})} TLS^{i+1}_1$$ and that the $SITT_{i}^{\{p(|id|)\}}$-definable in $TLS^i_1$ (resp. $SITT_{i}^{\{2^{p(||id||)}\}}$-definable in $TSC^i_1$) multifunctions are $L_1$-$FLOGSPACE^{SIT_{i,1}}[wit]$ (resp. $L_1$-$FSC^{SIT_{i,1}}[wit]$). These multifunction classes are respectively the logspace or $SC$ (poly-time, polylog-space) computable multifunctions whose output is bound by a term in $L_1$ and that have access to a witness oracle for another restriction on the $Σ^{\mathsf b}_{i}$ formulas, $SIT_{i,1}$. For the $i=1$ cases, this simplifies respectively to the functions in logspace and $SC$, Steve's Class, poly-time, polylog-space. We prove independence results related to the Matiyasevich Robinson Davis Putnam Theorem (MRDP) and to whether our theories prove simultaneous nondeterministic polynomial time, sublinear space is equal to co-nondeterministic polynomial time, sublinear space.

cs.LO↗
arXiv2026

TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

The verification of liveness conditions is an important aspect of state-based rigorous methods. This article addresses the extension of the logic of Event-B to a powerful logic, in which properties of traces of an Event-B machine can be expressed. However, all formulae of this logic are still interpreted over states of an Event-B machine rather than traces. The logic exploits that for an Event-B machine $M$ a state $S$ determines all traces of $M$ starting in $S$. We identify a fragment called TREBL of this logic, in which all liveness conditions of interest can be expressed, and define a set of sound derivation rules for the fragment. We further show relative completeness of these derivation rules in the sense that for every valid entailment of a formula $φ$ one can find a derivation, provided the machine $M$ is sufficiently refined. The decisive property is that certain variant terms must be definable in the refined machine. We show that such refinements always exist. Throughout the article several examples from the field of security are used to illustrate the theory.

cs.LO↗
arXiv2026

Scenes: A Meta-Logical Algebra for Mutable State

Modelling of mutable state spaces and precisely describing how variables are manipulated in a program is a fundamental problem in compositional verification. Though we can make use of the embedded abstract syntax of a program for such analysis, this runs contrary to the shallow-embedding approach, and hampers efficient proof automation. On the other hand, lenses and prisms provide an elegant algebraic foundation for modelling state, which provide sufficient structure to provide meta-logical program analysis, but without requiring a deep embedding. Nevertheless lenses, as complex algebraic objects, cannot easily be combined, complemented, or collected in sets. In this paper we contribute an accompanying algebraic structure called the scene, which allows us to characterise the set of variables, or coordinates, in a state space. Scenes intuitively correspond to sets of lenses, but like lenses they are purely semantic algebraic objects. We demonstrate that scenes provide us with sufficient structure to characterise the lens-based meta-logical properties, like independence and equivalence. Moreover, we introduce the notion of a scene space, analogous to a vector space, which allows us to recover a set-like algebraic structure. Finally, we show how scenes allow us to characterise the free and bound variables of expressions and programs, without any need for syntax, and demonstrate their use for reasoning about programs by deriving reasoning principles for the parallel composition operator.

cs.LO↗