Email Gateway (Mar 17 2026 at 13:25): Email Gateway (Mar 17 2026 at 13:25):From: Tobias Nipkow <nipkow@in.tum.de>
Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity
Necessity Proof in Isabelle/HOL
Kim, Yong-Dock
This study reconstructs metaphysical arguments within a framework of
computational formalization and machine verification, thereby recasting
ontological claims as candidates for formal validation.
This paper presents a formal development in automated reasoning for metaphysical
systems, treating ontological arguments as precisely specified logical theories
subject to machine verification. We provide an Isabelle/HOL formalization that
reconstructs and verifies the core claims of two prior philosophical arguments
within higher-order logic.
Working entirely within HOL and introducing no additional axioms beyond the base
logic, the development proceeds by conservative definitional extension (U-layer
methodology). We define the concept of H-Optimality () — capturing the ultimate
truth concept of "a truth so certain that no more certain truth can be
conceived" — as a structurally maximal admissible ground characterized by
maximal non-trivial support relations and a finality condition.
A Hilbert-style flat-model interpretation establishes the internal consistency
and non-vacuity of this definitional package. This confirmation of the concept's
consistency fulfills the core objective pursued by ontological arguments since
G. W. Leibniz. Within this framework, we formally derive structural exclusion
results for at the level of argument-classes: the cases (singularity), (strict
duality), and independent maxima are ruled out by -collapse (-equivalence
collapse) and -collapse (numerical-identity collapse) mechanisms. Consequently,
emerges as the unique admissible cardinality compatible with the stated
maximality and exclusion conditions.
We further prove a Definitional Finality Theorem: assuming and that any
definition ranges over the pan-domain (), there does not exist an satisfying
such that . This establishes a precise formal boundary for admissible
strengthening under the given definitions, proving that the definition of a
truth strictly superior to is impossible.
Finally, bounded finite-model search (Nitpick) identifies a genuine satisfying
model, providing mechanized evidence for the existence of a non-vacuous and
genuine triune model.
https://www.isa-afp.org/entries/Axiom_Free_Ontological_Trinity.html
Last updated: Mar 21 2026 at 20:30 UTC