Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL

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 ($H_{opt}$) — 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 $H_{opt}$ at the level of argument-classes: the cases $N=1$ (singularity), $N=2$ (strict duality), and $N \ge 4$ independent maxima are ruled out by $\approx$-collapse ($\mathrm{Arg}$-equivalence collapse) and $=$-collapse (numerical-identity collapse) mechanisms. Consequently, $N=3$ emerges as the unique admissible cardinality compatible with the stated maximality and exclusion conditions.

We further prove a Definitional Finality Theorem: assuming $H_{opt}(q)$ and that any definition $D$ ranges over the pan-domain ($\mathrm{PDom}$), there does not exist an $r$ satisfying $D(r)$ such that $\mathrm{Arg}(q) \prec \mathrm{Arg}(r)$. This establishes a precise formal boundary for admissible strengthening under the given definitions, proving that the definition of a truth strictly superior to $H_{opt}$ 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.