Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.26806

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

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 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ödel'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ödel'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.

Explore related subjects

cs.LOcs.AI

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Christoph Benzmüller. 2026-09-25. Gödel's and Scott's Variants of the Ontological Argument in Lean 4 and TPTP THF. 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

Encoder-Decoder Transformers: Logical Characterizations and Periodicity

We give logical characterizations of encoder-decoder transformers, the foundational architecture for LLMs that also sees use in various settings that benefit from cross-attention, in the practical setting of floating-point numbers and soft attention. First, we characterize such transformers via a new temporal logic that extends propositional logic with a counting global modality over the encoder input and a past modality over the decoder input, as well as via a type of distributed automata. We consider three frameworks: with and without a final softmax step in the transformer, and in the setting where each model generates tokens via autoregression. Second, we show that both autoregressive transformers and sentences of counting propositional logic - the fragment of the previous logic obtained by omitting the past modality - recognize exactly the commutative star-free languages. Finally, we find that the sequences of tokens the transformers generate are ultimately periodic (and each token appears in the period at most once). This allows us to characterize autoregressive transformers via sentences of counting propositional logic that generate tokens without autoregression, i.e., we can effectively eliminate recursion from the transformers.

cs.LO↗
arXiv2026

Rice's Theorem under Self-Modification: Elevation Operators and a Normal Form

We ask whether it can be certified algorithmically that a self-modifying program keeps a behavioural property, a safety property in the motivating case, after its next rewrite (preservation) and along its whole evolution (persistence). When the rewrite depends only on behaviour, preservation is a behavioural property and Rice's theorem applies. When the rewrite reads the code, preservation is no longer behavioural; yet, under a uniform disruption condition, the s-m-n reduction that proves Rice's theorem works inside a single class of behaviourally identical programs, and preservation inherits the degree of the halting problem. One step never exceeds the degree of the property, while persistence can climb one level of the arithmetical hierarchy. We then isolate the mechanism shared by rewriting, supervision and system comparison, the elevation operator, and prove a normal form: the preserving set is determined by a single finite trigger and a polarity, and the Rice-Shapiro theorem restricts the polarity to the arithmetical class of the property. Runtime monitors, consistency supervision, conformance to a reference and observational equivalence are instances, and no sound theory covers the preserving systems.

cs.LO↗
arXiv2026

Coinductive reasoning for parametrized functors and monads

Lax extensions (also called relators or relation liftings) are a categorical notion to reason about functors acting on functions and relations in a compatible way. They play a central role to develop sound proof principles for behavioral equivalence of state-based systems and are also important for establishing contextual equivalence for effectful programs. In this paper, we develop the theory of lax extensions for parametrized functors and monads and consider notions of behavioral preorders, equivalence relations or metrics which can now be modulated by additional parameters. From an operational viewpoint, we replace standard contextual equivalence where we quantify over all possible contexts by a refined notion of equivalence where the user can regulate the allowed contexts via chosen parameters.

cs.LO↗