\documentclass[11pt]{amsart} \usepackage[T1]{fontenc} \usepackage{lmodern,amssymb,mathtools,microtype,booktabs,longtable,listings} \usepackage[margin=1.1in]{geometry} \usepackage{xcolor} \usepackage{eso-pic,graphicx} \definecolor{citationcyan}{RGB}{0,150,180} \definecolor{equationorange}{RGB}{220,100,0} \definecolor{definitionblue}{RGB}{0,90,190} \definecolor{definitionred}{RGB}{190,0,30} \definecolor{sectionlinksilver}{RGB}{128,128,128} \usepackage[colorlinks=true,linkcolor=definitionblue,citecolor=citationcyan,urlcolor=citationcyan,hypertexnames=false]{hyperref} \let\originaleqref\eqref \newcommand{\mathref}[1]{{\hypersetup{linkcolor=equationorange}\originaleqref{#1}}} \newcommand{\defref}[1]{{\hypersetup{linkcolor=definitionred}\originaleqref{#1}}} \newtheorem{theorem}{Theorem}[section] \newtheorem{lemma}[theorem]{Lemma} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \numberwithin{equation}{section} \setcounter{tocdepth}{1} \newcommand{\God}{\mathsf G} \newcommand{\Pos}{\mathsf P} \newcommand{\Ess}{\mathsf{Ess}} \newcommand{\NE}{\mathsf{NE}} \newcommand{\Con}{\operatorname{Con}} \newcommand{\Prov}{\operatorname{Prov}} \newcommand{\Pow}{\mathcal P} \title[Necessary existence in the Godel--Scott framework]{A G\"odel--Scott theorem of necessary existence} \author{OpenAI} \date{September 16, 2026} \hypersetup{pdfauthor={OpenAI},pdftitle={A Godel-Scott theorem of necessary existence}} \begin{document} \AddToShipoutPictureFG*{% \AtPageLowerLeft{% \raisebox{0.38\paperheight}{% \hspace{0.24in}% \rotatebox{90}{% \href{https://godexists.prof}{\color{gray}\small godexists.prof/0000.0001 16 Sep 2026}% }% }% }% } \maketitle \noindent\textbf{Does God exists?} \medskip We formulate the question as an existence problem in a specified higher-order modal theory. The resulting theorem is affirmative: the G\"odel--Scott axioms imply necessary realization of a unique God-like individual. The proof below is followed by its algebraic and proof-theoretic consequences, and a probability-logic formulation. {\hypersetup{linkcolor=sectionlinksilver}\tableofcontents} \section{The theorem and its setting.} \subsection{The mathematical claim.} Let $\Gamma$ denote the axiom schemas and definitions in \S2, imposed globally on an S5 frame. The property $\God$ is the defined God-like predicate of that theory. We prove \begin{equation}\label{mainclaim} \Gamma\models_{\mathrm{S5}}\Box\exists!x\God(x). \end{equation} Since S5 frames are reflexive, \mathref{mainclaim} implies $\exists!x\God(x)$ at the distinguished actual world of every model. This is a theorem of mathematical logic. Its probability formulation is a separate corollary of entailment, not an additional assumption in the existence proof. The framework is specifically the consistent \emph{Scott amendment} of G\"odel's ontological schema. The possession condition in the definition of essence is retained. The initial formalization \cite{b29,r7,a168} and the later analysis by Benzm\"uller and Scott \cite{b2,a32} provide the central reference points. Alternative formulations are considered only in the survey; they are not combined with the main axioms. \subsection{Interpretation and proof obligation.} An interpretation of $\God$ as a creator or an omniscient personal being is not a primitive theorem of logic. Here the word God-like is fixed by Definition~\defref{defG}. Thus the affirmative theorem has a determinate mathematical object and a determinate class of structures. An assertion about the actual universe additionally requires identifying its intended interpretation with a model of these axioms. The equation $\Pr(H\mid\Gamma)=1$ does not imply $\Pr(H)=1$ in an unspecified probability space. Section~7 gives the precise probability-space formulation. \subsection{Organization.} The proof proceeds from possible realization to essence, then from essence to necessary realization. Uniqueness and a principal-ultrafilter description follow from the same assumptions. We next exhibit models, characterize the full-property case, and explain why omitting the essence conjunct yields inconsistency. Incompleteness concerns the internal proof theory of effective arithmetic extensions; probability logic then translates semantic entailment into a universal conditional-certainty assertion. The research survey follows those same dependencies. \section{Language, semantics, and axioms.} \subsection{Worlds and properties.} Fix nonempty sets $W$ and $D$, a distinguished world $w_0\in W$, and an equivalence relation $R\subseteq W\times W$. Individuals belong to the constant domain $D$. An intensional unary property is a function \[ \varphi:W\times D\longrightarrow\{0,1\}. \] We initially use full property quantification. Consequently all complements, conjunctions, identity properties, and world-dependent properties used below are available. Write $\varphi(x)$ for evaluation at the current world. Identity on $D$ is rigid. The modal operators have the usual Kripke interpretation: \begin{align} \mathcal M,w\models\Box A &\iff \forall v\,(wRv\Rightarrow\mathcal M,v\models A),\label{box}\\ \mathcal M,w\models\Diamond A &\iff \exists v\,(wRv\land\mathcal M,v\models A). \end{align} A universally valid schema holds at every world for every admissible assignment. Property variables retain their intensions when moving between worlds. This prevents an implicit switch between a property and its extension at one world. \begin{lemma}\label{s5lemma} Every S5 frame validates \[ \Diamond\Box A\to\Box A,\qquad \Box A\to A. \] \end{lemma} \begin{proof} If $wRv$, the equivalence classes of $w$ and $v$ coincide. Thus, if $A$ holds at all worlds accessible from such a $v$, it holds at all worlds accessible from $w$. Reflexivity gives the second implication. \end{proof} These frame conditions are sufficient for the present derivation; no minimality claim is made. Published work also verifies a Scott-style theorem in KB \cite{a168}. General-model semantics and weaker property comprehensions are discussed in \S8. \subsection{The G\"odel--Scott definitions.} Let $\Pos(\varphi)$ be a primitive positivity predicate, potentially evaluated at each world. It is an abstract mathematical predicate, not a numerical sign or a moral judgment. Define \begin{align} \God(x)&\iff\forall\varphi\,[\Pos(\varphi)\to\varphi(x)],\label{defG}\\ \Ess(\varphi,x)&\iff\varphi(x)\land \forall\psi\,[\psi(x)\to\Box\forall y(\varphi(y)\to\psi(y))],\label{defEss}\\ \NE(x)&\iff\forall\varphi\,[\Ess(\varphi,x)\to\Box\exists y\varphi(y)].\label{defNE} \end{align} The definitions are global. In \defref{defEss} the conjunct $\varphi(x)$ is essential to the precise system being studied. Equation \defref{defNE} defines necessary existence through necessary exemplification of essences; we use that equation rather than infer existence from the name of the predicate. \subsection{The axioms.} For $\neg\varphi:=\lambda x.\neg\varphi(x)$, impose \begin{align} \Pos(\neg\varphi)&\iff\neg\Pos(\varphi),\tag{A1}\label{A1}\\ \Pos(\varphi)\land\Box\forall x(\varphi(x)\to\psi(x))&\to\Pos(\psi),\tag{A2}\label{A2}\\ &\Pos(\God),\tag{A3}\label{A3}\\ \Pos(\varphi)&\to\Box\Pos(\varphi),\tag{A4}\label{A4}\\ &\Pos(\NE).\tag{A5}\label{A5} \end{align} All free property variables are universally quantified. All five schemas hold at every world. Globality is needed when the existence argument moves to an accessible world. A1 chooses exactly one property from each complementary pair. A2 closes positivity under necessary implication. A3 declares the joint God-like property positive. A4 makes positive status persistent over accessibility. A5 declares the defined necessary-existence property positive. These are the hypotheses of the existence theorem. \section{The existence proof.} \subsection{Possible realization.} \begin{lemma}\label{possible} At every world, $\Pos(\varphi)\to\Diamond\exists x\varphi(x)$. \end{lemma} \begin{proof} Assume $\Pos(\varphi)$ but $\neg\Diamond\exists x\varphi(x)$. Then $\Box\forall x\neg\varphi(x)$, hence \[ \Box\forall x(\varphi(x)\to\neg\varphi(x)). \] A2 yields $\Pos(\neg\varphi)$ and A1 yields $\neg\Pos(\varphi)$, a contradiction. \end{proof} \begin{corollary}\label{possibleG} $\Diamond\exists x\God(x)$ holds at every world. \end{corollary} \begin{proof} Apply Lemma~\ref{possible} to A3. \end{proof} The corollary does not infer joint possibility from separate possibilities. That inference would be invalid: a property and its complement can be separately realizable without being jointly realizable. The joint property appears explicitly in A3. \subsection{Essence.} \begin{lemma}\label{possessed} If $\God(a)$, then for every $\psi$, \[ \Pos(\psi)\iff\psi(a). \] \end{lemma} \begin{proof} The forward implication is Definition~\defref{defG}. Conversely, if $\psi(a)$ and $\neg\Pos(\psi)$, A1 gives $\Pos(\neg\psi)$; Definition~\defref{defG} gives $\neg\psi(a)$, a contradiction. \end{proof} \begin{lemma}\label{essence} $\God(a)\to\Ess(\God,a)$. \end{lemma} \begin{proof} Assume $\God(a)$ at $w$. For any $\psi$ with $\psi(a)$ there, Lemma~\ref{possessed} yields $\Pos(\psi)$. A4 yields $\Box\Pos(\psi)$. At each accessible world, Definition~\defref{defG} gives $\forall y(\God(y)\to\psi(y))$. Thus the second conjunct of \defref{defEss} holds for $\varphi=\God$, and the first conjunct is the initial assumption. \end{proof} \subsection{Necessary realization.} \begin{lemma}\label{upgrade} At every world, $\exists x\God(x)\to\Box\exists x\God(x)$. \end{lemma} \begin{proof} Choose $a$ with $\God(a)$. A5 and \defref{defG} give $\NE(a)$. Lemma~\ref{essence} gives $\Ess(\God,a)$. Definition~\defref{defNE} therefore gives $\Box\exists y\God(y)$. \end{proof} \begin{theorem}[G\"odel--Scott necessary existence]\label{existence} Every model of $\Gamma$ satisfies $\Box\exists x\God(x)$ at every world. It therefore satisfies $\exists x\God(x)$ at its distinguished actual world. \end{theorem} \begin{proof} Corollary~\ref{possibleG} supplies an accessible world containing a God-like individual. At that world Lemma~\ref{upgrade} gives $\Box\exists x\God(x)$. Hence the original world satisfies $\Diamond\Box\exists x\God(x)$. Lemma~\ref{s5lemma} yields necessity and then actual-world realization. \end{proof} \begin{theorem}[Uniqueness]\label{uniqueness} $\Gamma\models\Box\exists!x\God(x)$. \end{theorem} \begin{proof} At any world suppose $\God(a)$ and $\God(b)$. The identity property $I_a(x):=(x=a)$ is admissible. Since $I_a(a)$ holds, Lemma~\ref{possessed} gives $\Pos(I_a)$. Definition~\defref{defG} gives $I_a(b)$, so $b=a$. Apply this at each accessible world and use Theorem~\ref{existence}. \end{proof} Theorems~\ref{existence} and~\ref{uniqueness} establish the main claim. The following sections develop its algebraic, model-theoretic, and probabilistic consequences. \section{Algebraic structure and the role of infinity.} \subsection{Positive properties as evaluation.} Fix a world $w$ and let $g_w$ be its unique God-like individual. By Lemma~\ref{possessed}, \begin{equation}\label{evaluation} \Pos_w(\varphi)\iff\varphi(w,g_w)=1. \end{equation} Consequently the positive properties form a principal ultrafilter on the Boolean algebra of all subsets of $W\times D$, with principal point $(w,g_w)$. \begin{proposition}\label{filter} Write $U_w=\{\varphi:\Pos_w(\varphi)\}$. Then $\top\in U_w$, $\bot\notin U_w$, $U_w$ is upward closed for pointwise implication and closed under finite conjunction, and exactly one of $\varphi,\neg\varphi$ belongs to $U_w$. \end{proposition} \begin{proof} By \mathref{evaluation}, membership means truth at the point $(w,g_w)$. Each assertion follows by the corresponding Boolean truth rule at that point. For example, if $\varphi,\psi\in U_w$, both are true there, so $\varphi\land\psi\in U_w$. \end{proof} \begin{proposition}\label{intersection} In full property semantics, \[ \bigcap_{\varphi\in U_w}\{(v,x):\varphi(v,x)=1\}=\{(w,g_w)\}. \] \end{proposition} \begin{proof} Every member of $U_w$ contains $(w,g_w)$ by \mathref{evaluation}. Conversely, the singleton property of $(w,g_w)$ is available under full property quantification and belongs to $U_w$ by the same equation. The intersection is therefore no larger than that singleton. \end{proof} These are consequences of the modal theorem, not a replacement of its modal premises by bare ultrafilter existence. The distinction matters: a principal ultrafilter alone says nothing about how its generator varies with the world. Research on modal ultrafilters makes this distinction explicit \cite{r35,b0,b3}. \subsection{Why a general ultrafilter is insufficient.} \begin{definition} An ultrafilter $U$ on a set $X$ is a proper filter on $\Pow(X)$ which, for every $A\subseteq X$, contains exactly one of $A$ and $X\setminus A$. It is principal if $U=\{A:x\in A\}$ for some $x\in X$. \end{definition} \begin{proposition}\label{finiteprincipal} Every ultrafilter on a finite nonempty set is principal. \end{proposition} \begin{proof} If no singleton belongs to $U$, the complement of every singleton belongs to $U$. Intersect these finitely many complements. Their intersection is empty, contradicting propriety of the filter. Thus $\{x\}\in U$ for some $x$. Upward closure and propriety show $A\in U$ exactly when $x\in A$. \end{proof} \begin{proposition}\label{nonprincipal} Assuming the ultrafilter lemma, there is an ultrafilter on $\mathbb N$ with empty intersection of all its members. \end{proposition} \begin{proof} Extend the cofinite filter to an ultrafilter $U$. For each $n$, the set $\mathbb N\setminus\{n\}$ is cofinite and belongs to $U$. Thus no $n$ belongs to the intersection. Moreover, $U$ contains no finite set: intersecting such a set with its cofinite complement would give the empty set. \end{proof} Finite conjunction closure therefore does not imply simultaneous realization of an arbitrary infinite family. \subsection{Stone representation and what it represents.} Let $B$ be a Boolean algebra and $\operatorname{Ult}(B)$ its set of ultrafilters. Define \[ \widehat b=\{U\in\operatorname{Ult}(B):b\in U\}. \] Under the Boolean prime ideal theorem, the map $b\mapsto\widehat b$ is an injective Boolean homomorphism, the algebraic core of Stone representation \cite{stone}. \begin{proof}[Proof of the stated representation fact] The Boolean operations are preserved by the ultrafilter laws. If $b\ne c$, then their symmetric difference $d$ is nonzero. Extend the proper filter generated by $d$ to an ultrafilter $U$. Then $d\in U$, so exactly one of $b,c$ belongs to $U$. Hence $\widehat b\ne\widehat c$. \end{proof} Representation supplies points in a space of ultrafilters. It does not identify them with individuals in an independently prescribed physical domain. In the G\"odel--Scott theorem, \mathref{evaluation} supplies the particular evaluation point only after the modal existence proof has been completed. \section{Models, collapse, and the essence amendment.} \subsection{A nonvacuity witness.} \begin{proposition}\label{singletonmodel} $\Gamma$ has a model. \end{proposition} \begin{proof} Take $W=\{w\}$, $D=\{d\}$ and $R=\{(w,w)\}$. Set $\Pos(\varphi)$ iff $\varphi(w,d)=1$. A1, A2 and A4 follow immediately. Every positive property holds of $d$, so $\God(d)$ and A3 hold. Every essence of $d$ holds of $d$ by \defref{defEss}, and is consequently exemplified at the sole accessible world. Thus $\NE(d)$ and A5 hold. \end{proof} The existence result is therefore not justified merely by explosion from an inconsistent theory. For a sound proof calculus, Proposition~\ref{singletonmodel} establishes consistency externally in the surrounding metatheory. \subsection{Modal collapse.} \begin{proposition}\label{collapse} For every proposition $p$ for which $\lambda x.p$ is an admissible property, \[ \Gamma\models p\to\Box p. \] \end{proposition} \begin{proof} At a world where $p$ holds, choose $a$ with $\God(a)$ by Theorem~\ref{existence}. For $\psi(x):=p$, we have $\psi(a)$. Lemma~\ref{essence} gives $\Box\forall y(\God(y)\to p)$. Theorem~\ref{existence} also gives $\Box\exists y\God(y)$. Together they imply $\Box p$. \end{proof} Modal collapse is a consequence of the stated axioms and distinguishes this theory from collapse-free variants \cite{r109,r35,a129,b7}. \subsection{Classification under full property quantification.} \begin{theorem}\label{classification} In the full-property semantics of \S2, a structure satisfies $\Gamma$ if and only if $R$ is the identity relation and there is a function $g:W\to D$ such that \begin{equation}\label{classformula} \Pos_w(\varphi)\iff\varphi(w,g(w)). \end{equation} The defined predicates are interpreted by \defref{defG}--\defref{defNE}. \end{theorem} \begin{proof} Suppose first that $\Gamma$ holds. Uniqueness defines $g(w)$ without choosing between multiple witnesses. Equation \mathref{classformula} is Lemma~\ref{possessed}. If $wRv$ and $w\ne v$, use the admissible property $\psi(u,x):=(u=w)$. It holds of $g(w)$ at $w$. Lemma~\ref{essence} implies that every God-like individual at $v$ has $\psi$ there. Theorem~\ref{existence} supplies such an individual, but $\psi(v,x)$ is false. This contradiction excludes distinct accessible worlds. Reflexivity then makes $R$ the identity. Conversely, let $R$ be the identity and define positivity by \mathref{classformula}. A1 and A2 follow from evaluation at $(w,g(w))$, and A4 holds since the only accessible world is $w$. Definition~\defref{defG} gives $\God(w,x)$ iff $x=g(w)$: the forward direction uses the identity property of $g(w)$ and the reverse direction uses evaluation. Thus A3 holds. For any $x$, every essence of $x$ holds of $x$ at $w$, so it has a witness in the only accessible world. Hence $\NE(w,x)$ holds for all $x$, establishing A5. \end{proof} The classification is specific to full property quantification, particularly the world-separating properties used in its proof. For a restricted semantic language, truth-indiscernible worlds need not be identical. The theorem is not asserted for every G\"odelian variant or every Henkin property domain. \begin{corollary}\label{countmodels} On fixed finite carriers with $|W|=k\ge1$ and $|D|=n\ge1$, the full-property S5 models of $\Gamma$ have identity accessibility and exactly $n^k$ possible positivity interpretations. \end{corollary} \begin{proof} By Theorem~\ref{classification}, models correspond exactly to functions $g:W\to D$. There are $n^k$ such functions. Distinct functions give different positivity predicates, as identity properties distinguish their values. \end{proof} This further shows why $\Box\exists!x\God(x)$ should not be read as a claim that the same individual is God-like in every world of a disconnected frame. A function $g$ can take different values in different components. The theorem's necessity ranges over accessibility. \subsection{Why the unamended essence definition fails here.} Replace \defref{defEss} by \[ \Ess^{-}(\varphi,x)\iff \forall\psi\,[\psi(x)\to\Box\forall y(\varphi(y)\to\psi(y))] \] and define $\NE^{-}$ by using $\Ess^{-}$ in \defref{defNE}. \begin{proposition}\label{emptyessence} In the same S5 setting, A1, A2 and $\Pos(\NE^{-})$ are inconsistent with these unamended definitions. \end{proposition} \begin{proof} The false property $\bot$ necessarily implies every property, so $\Ess^{-}(\bot,x)$ holds for every $x$. Therefore $\NE^{-}(x)$ would imply $\Box\exists y\bot$, which is false on a reflexive frame. Thus $\NE^{-}$ has no possible instance. But the proof of Lemma~\ref{possible}, using only A1 and A2, shows that a positive property must have a possible instance. Apply it to $\Pos(\NE^{-})$ for a contradiction. \end{proof} This explains why the corrected Scott framework is specified from the outset. The research literature supplies more general analyses of the inconsistency \cite{r9,r108}; the argument above proves precisely the S5 claim needed here. \section{Proof theory, compactness, and incompleteness.} \subsection{An existence theorem is not an internal consistency oracle.} Let $T$ be a consistent, effectively axiomatized classical theory extending sufficient arithmetic for the standard incompleteness theorems. If the modal proof is implemented in $T$, distinguish the encoded modal object theory from its arithmetic metatheory. A claim of full higher-order semantic completeness is not part of this implementation assumption. The first incompleteness theorem, in Rosser's strengthening, supplies an arithmetic sentence $\sigma$ such that \begin{equation}\label{incomplete} T\nvdash\sigma,\qquad T\nvdash\neg\sigma. \end{equation} The second theorem, with standard arithmetized provability and sufficient arithmetic, yields \begin{equation}\label{second} T\nvdash\Con(T). \end{equation} The original and formalized sources are \cite{r92,rosser,a91,a166}. The hypotheses are essential: these are theorems about effective theories with arithmetic strength, not every collection of mathematical truths. \begin{proposition}\label{consistencybarrier} If $T\vdash H$ and $T$ satisfies the hypotheses of \mathref{second}, then $T\nvdash H\to\Con(T)$. \end{proposition} \begin{proof} Otherwise modus ponens would give $T\vdash\Con(T)$, contradicting \mathref{second}. \end{proof} Thus a theory can prove its God-like existence sentence while remaining incomplete. Conversely, incompleteness does not supply a God-like existence sentence. A model construction in a stronger metatheory can establish consistency of a weaker theory without contradicting \mathref{second}; it is not that weaker theory's own internal consistency proof. \subsection{L\"ob's theorem and reflection.} With the standard Hilbert--Bernays--L\"ob derivability conditions, L\"ob's theorem states \[ T\vdash\Prov_T(\ulcorner A\urcorner)\to A \quad\Longrightarrow\quad T\vdash A. \] A formal development is included in \cite{a166}. Taking $A=\bot$ recovers the obstruction to a consistent $T$ proving its standard consistency sentence. \subsection{First-order compactness and witness construction.} The first-order compactness theorem states that a theory is satisfiable if each finite subset is satisfiable. It can be proved from completeness: an unsatisfiable theory proves contradiction, and a finite proof uses only finitely many premises. Foundational and formalized treatments appear in \cite{henkin,a27,a38,a164,a55}. For a family of properties $\{P_i:i\in I\}$ in a first-order language, add a constant $c$. If every finite subset of \[ B\cup\{P_i(c):i\in I\} \] is satisfiable, compactness supplies some model realizing the entire family. It does not guarantee a witness in a prescribed model. In the standard natural numbers the requirements $c>n$ for all standard $n$ are finitely satisfiable but have no joint witness. A compactness model of arithmetic may instead contain a nonstandard element. This directly explains two restrictions in the ontological proof. First, individual realizability cannot replace finite joint realizability. Second, existence in some mathematical structure does not identify that structure with the actual universe. Full second-order semantics also cannot inherit first-order compactness without justification. Henkin's general-model treatment of type theory \cite{r89,r90,r91,a1} concerns a different semantic completeness claim. \subsection{A separation theorem.} \begin{proposition}\label{separation} If $T_0$ is any satisfiable first-order theory and $U$ is a fresh unary predicate with no connecting axioms, then $T_0$ entails neither $\exists xU(x)$ nor its negation. \end{proposition} \begin{proof} Take $\mathcal M\models T_0$ with nonempty domain $M$. Interpret $U$ as $\varnothing$ in one expansion and as $M$ in another. All sentences of $T_0$ retain their truth values, while the existential assertion is respectively false and true. \end{proof} The construction applies to any satisfiable theory in the original language. An existence assertion about the new predicate requires connecting axioms. The G\"odel--Scott definitions and axioms provide such structure explicitly. \subsection{Material implication and explosion.} Put $H:=\exists x\God(x)$ and let $Q$ be an uninterpreted predicate. Once Theorem~\ref{existence} is established, \begin{equation}\label{permission} \Gamma\models\neg H\to\forall aQ(a) \end{equation} is a truth-functional consequence for every interpretation of $Q$. Hence the sentence ``If there is no God, everything is permitted'' can be represented by \mathref{permission}, but it is not an independent mathematical input. No moral properties of $Q$ are assumed. Likewise, classical explosion says $A,\neg A\vdash B$ for every $B$: infer $A\lor B$ and use $\neg A$. Explosion concerns contradiction, not absence of a deity. Proposition~\ref{singletonmodel} ensures that the main theorem is not merely an application of explosion. This is the relevant formal connection among the permission sentence, consistency, and the existence proof. \section{From entailment to probability.} \subsection{Certainty conditional on the model class.} Let $\Omega$ be a nonempty set of pointed models of $\Gamma$, and equip it with any probability measure $\mu$. Write \[ E_H=\{(\mathcal M,w)\in\Omega:\mathcal M,w\models H\}. \] \begin{theorem}\label{probone} For every such probability space, $\mu(E_H)=1$. \end{theorem} \begin{proof} Theorem~\ref{existence} gives $E_H=\Omega$. It is therefore measurable and has measure one. \end{proof} More generally, on a specified probability space of structures, let $E_\Gamma$ be the measurable event that all the stipulated axioms hold globally. If $\mu(E_\Gamma)>0$ and $E_H$ is measurable, then \begin{equation}\label{conditionalprob} \mu(E_H\mid E_\Gamma)= \frac{\mu(E_H\cap E_\Gamma)}{\mu(E_\Gamma)}=1. \end{equation} This follows from $E_\Gamma\subseteq E_H$ and holds for every probability measure satisfying the stated conditions. \subsection{A quantitative entailment bound.} Probability logic provides a useful generalization, related to Suppes-style results \cite{a53,a52}. Suppose measurable events $A_1,\ldots,A_m,H$ satisfy $\bigcap_i A_i\subseteq H$. \begin{proposition}\label{unionbound} For any probability measure, \[ \Pr(H)\ge1-\sum_{i=1}^m\Pr(A_i^c). \] \end{proposition} \begin{proof} The assumed inclusion implies $H^c\subseteq\bigcup_i A_i^c$. Monotonicity and the union bound give $\Pr(H^c)\le\sum_i\Pr(A_i^c)$; subtract from one. \end{proof} No independence assumption is needed. If numerical bounds $\Pr(A_i^c)\le\varepsilon_i$ were independently justified, the theorem would yield $\Pr(H)\ge1-\sum_i\varepsilon_i$. The present analysis provides no empirical values for those $\varepsilon_i$. Setting all of them to zero amounts to concentrating the measure on models satisfying the axioms, as in Theorem~\ref{probone}. \subsection{Why the conditioning cannot be discarded.} \begin{proposition}\label{arbitraryprob} The probability axioms alone allow every value in $[0,1]$ for a fresh, unconstrained existence predicate. \end{proposition} \begin{proof} Use the two expansions $\mathcal M_0,\mathcal M_1$ from Proposition~\ref{separation}. For any $r\in[0,1]$, put probability $1-r$ on $\mathcal M_0$ and $r$ on $\mathcal M_1$, with all subsets measurable. Then $\Pr(\exists xU(x))=r$. \end{proof} Thus \mathref{conditionalprob} specifies a conditional probability; the probability axioms alone do not determine an unconditional value for an unconstrained existence assertion. \section{A connected research survey.} \subsection{Scope and evidential status.} The 202 references below document the proof's mathematical context and possible verification routes. They are not 202 independent proofs of the conclusion, nor are all 202 required premises. Each reference has a research-role annotation. The collection includes journal articles, books or chapters, historical texts, formal proof developments, and a small number of preprints or conference communications. Access labels distinguish the evidence actually available: \emph{F} means relevant full-text passages were consulted; \emph{A} means the primary abstract and bibliographic record were consulted; \emph{B} means bibliographic-level evidence only, from a DOI registry, author-maintained record, or cited scholarly bibliography. A B entry is a research lead, not evidence that its entire argument was checked. There are 7 F, 98 A, and 97 B entries. The self-contained deductions above do not depend on attributing uninspected technical results to B entries. The selected literature has a cutoff of September 14, 2026. \subsection{The precise G\"odelian lineage.} The primary G\"odel and Scott texts \cite{r5,r6}, their editorial and historical context \cite{r1,r2,r4,r40}, and the systematic discussions \cite{r3,r110} explain why the version must be named. An ontological argument is not a single interchangeable list of formulas. A change to essence, quantification, positivity, or modal strength can change its consistency and its consequences. The early computational work \cite{b29,b37,r7,a168,r33,r36} and the 2025 paper with its associated formal development \cite{b2,a32} establish a lineage for comparing explicit definitions. The relevant use of that literature is to select and check a precise formal system. It does not turn the authority of the authors into an additional axiom. Proposition~\ref{emptyessence} supplies the specific inconsistency calculation used in this manuscript. \subsection{Variants and axiom sensitivity.} Anderson, Anderson--Gettings, and H\'ajek proposed related modifications \cite{r12,r13,r14,r15,r16,r18}. Computer-assisted comparisons \cite{r32,r34} make it possible to test which assumptions are redundant or independent only after fixing the surrounding logic and domain conventions. Fitting's intensional treatment and its formal development \cite{r17,a129} are particularly relevant to the separation between a property's intension and its extension. The 2020 ultrafilter comparison reports collapse-free Anderson and Fitting variants \cite{r35}; simplified variants are documented in \cite{b7,b10,a74}. Those are useful comparison results, not a license to retain their advantages while silently using Scott's premises. Other reconstructed arguments, including Lowe's and Leibniz-style approaches \cite{b16,a123,b24}, enter the survey as tests of representation and compatibility claims. None is spliced into Theorem~\ref{existence}. \subsection{Type theory and property construction.} The use of $\forall\varphi$ calls for a typed semantic foundation. Church's formulation and subsequent type-theoretic accounts \cite{r23,r24,r25,r27,r28} explain the functional treatment of predicates. Comprehension, descriptions, general models, and extensionality \cite{r26,r89,r90,r91,r93} determine which property constructions are legitimate. They are directly relevant to the identity property used for uniqueness and the world-separating property used for classification. Supporting formalizations cover substitution, binding, typed term algebra, and unification \cite{a9,a41,a111,a120,a125,a126}. These are not ornamental implementation details: an invalid substitution can turn a formally plausible derivation into a different formula. Higher-order term orderings \cite{a115,a136,a140} and rewriting results \cite{a21,a22,a23,a70,a135} support normalization and automation. They are background for a verified implementation, not new existence principles. Type restrictions and semantic fixed points \cite{a128,a174} also show why a convenient informal expression is not automatically available in every type system. \subsection{Modal semantics and quantifier domains.} Intensional and quantified modal logic \cite{r20,r21,r22,r96,r97,r101} supplies the semantics of \S2. Free-logic treatments \cite{r102,r103,r104,r105,a116} are relevant if one introduces a separate actual-existence predicate. Constant-domain quantification and actualist quantification should not be exchanged without rechecking definitions and proofs. Formal modal completeness and bisimulation developments \cite{a114,a18,a60,a104} clarify another boundary: a language may fail to distinguish worlds even when they are distinct in the underlying set. The classification theorem deliberately assumes enough properties to distinguish them. Temporal and nominal modal logics \cite{a137,a152} are comparisons of expressive power; their operators do not automatically satisfy S5. Nonclassical negation semantics \cite{a87,r98} show why the classical proof rules, including explosion and double-negation reasoning, must be stated rather than taken to hold in every logic. \subsection{Embeddings and preservation of meaning.} A shallow embedding represents modal propositions by functions on worlds; a deep embedding represents syntax explicitly. The foundational modal embedding \cite{r19}, subsequent metalogical work \cite{r29,b33}, and formal faithfulness studies \cite{a20,a2} address when the two representations agree. Faithfulness is the relevant theorem when moving from a displayed mathematical formula to a proof-assistant term. Recent formalizations of HOL within HOL and of Q0 completeness \cite{a0,a1,a44} sharpen the object-theory/metatheory distinction. They concern carefully specified general-model semantics and proof calculi. The proof checker for Isabelle's metalogic \cite{a84} and syntax-independent infrastructure \cite{a89} supply supporting foundations. Mechanized metaphysical theories \cite{r30,r106,r107,a124} illustrate the same point: verifying an encoding first requires fixing what the encoding means. \subsection{Boolean algebra, compactness, and model existence.} Stone representation \cite{stone} and free Boolean-algebra constructions \cite{a183} explain the algebraic vocabulary used in \S4. Boolean-subalgebra and axiom-equivalence developments \cite{a103,a181} are relevant when replacing a list of axioms by an apparently equivalent algebraic description. Such replacement needs a proof; the implication cannot be inferred from similar terminology. The recent modal-ultrafilter discussion \cite{b0,b3,b27} motivates caution about assigning modal collapse to bare filter structure. In this paper collapse is derived from the modal axioms, while the ultrafilter description follows from evaluation. Cardinal and ordinal resources \cite{a45,a185,a195} clarify the size of index sets and model families; finite equivalence-relation counting \cite{a145} relates to enumerating S5 frames. None supplies a measure on all conceivable worlds merely by establishing their cardinality. Henkin construction, compactness, maximal consistent sets, and abstract completeness \cite{henkin,a27,a38,a55,a164} are directly useful for proving that assumptions have models. Additional soundness and completeness developments \cite{a57,a61,a65,a71,a77,a106,a127,a131,a132,a193,a196,a197} show how different calculi support the same first-order semantic conclusions. These resources are foundations for independent checking, not extra theological evidence. \subsection{Arithmetic strength and self-reference.} G\"odel's and Rosser's results \cite{r92,rosser}, weak arithmetic \cite{a90}, finite-set coding \cite{a3,a167}, and abstract or concrete formalized incompleteness \cite{a91,a92,a93,a166} identify the assumptions behind \mathref{incomplete} and \mathref{second}. Set-theoretic model constructions \cite{a67,a98,a105} illustrate external and relative consistency methods. Goodstein computation \cite{a102} is a related example of the distinction between specifying a computation and proving a universal metatheoretic property. Work explicitly relating God-language and arithmetic \cite{r42,r111,r112} belongs to this discussion because additional axioms can link the subjects. Such links must be checked as hypotheses; Proposition~\ref{consistencybarrier} remains applicable whenever its own assumptions hold. \subsection{Proof search, certificates, and verification.} The published ontological formalizations use higher-order proof infrastructure, including Coq-oriented work \cite{r8,b30}. Isabelle, Coq, Lean, HOL4, HOL Light, PVS, Nuprl, and Agda are documented in \cite{r37,r45,r46,r47,r49,r50,r51,r52,r53}. Their inclusion supports comparison of proof environments; it does not assert that this manuscript was independently checked in every system. Search backends and calculi include resolution, superposition, higher-order tableaux, and paramodulation \cite{robinson,r76,r77,r78,r79,r80,r81,r82,r85,r88}. The verified resolution and clause-learning developments \cite{a19,a31,a34,a49,a112,a121,a141,a143,a151} concern the correctness of those methods. TPTP infrastructure and benchmark studies \cite{r72,r73,r74,r95}, solver integration \cite{r67,r75}, and countermodel generation \cite{r68} support reproducibility and diagnosis. Further proof-search and certificate resources \cite{a6,a16,a33,a47,a133,a146,a161,a169,a186} help distinguish a found derivation from a checked one. Restricted decision procedures and syntax representations \cite{a156,a157,a184,a192} delimit what finite or algorithmic testing can settle. General implementation discussions \cite{r10,r11,r48,r69,r70,r71,r86,r87} belong to this verification layer. Their role is methodological, and should not be mistaken for independent premises of the existence theorem. \subsection{Probability logic and semantic entailment.} The probability-logic entries \cite{a53,a52} are directly connected to Proposition~\ref{unionbound}: semantic implication constrains every admissible probability measure. Coproduct measures, higher-order conditional probability models, and certified density construction \cite{a39,a48,a158} concern how such measures can actually be specified. They do not select a unique measure over metaphysical interpretations. The modal theory proves existence; a model demonstrates nonvacuity; soundness explains the force of the proof; incompleteness limits internal self-certification; and probability logic yields certainty conditional on the stipulated theory. \section{Finite verification and reproducibility.} \subsection{A bounded independent check.} Theorem~\ref{classification} permits an elementary finite check independent of the written proof. For each finite carrier, enumerate all intensional properties and all positivity selections satisfying A1. Filter by A2 and A4, construct $\God$, $\Ess$ and $\NE$ from their definitions, and test A3 and A5. The table reports the resulting counts; every retained model satisfies existence and uniqueness. \begin{center} \begin{tabular}{cccr} \toprule Worlds & Individuals & Accessibility & Models of $\Gamma$\\ \midrule 1&1&Identity&1\\ 1&2&Identity&2\\ 1&3&Identity&3\\ 2&1&Identity&1\\ 2&1&Universal&0\\ 2&2&Identity&4\\ 2&2&Universal&0\\ \bottomrule \end{tabular} \end{center} The count concerns interpretations on fixed labelled carriers, not isomorphism classes. For two worlds, identity and universal accessibility exhaust the equivalence relations. The script below checks the reported finite cases. This finite enumeration does not prove the unbounded theorem; its proof is Theorem~\ref{classification}. No new Isabelle, Coq or Lean kernel-verification claim is made for this manuscript. \subsection{Executable specification.} The following Python 3 code uses only the standard library. Bit positions encode pairs $(w,x)$; every bit mask is one intensional property. \lstset{language=Python,basicstyle=\ttfamily\scriptsize,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false} \begin{lstlisting} from itertools import product def count_models(k,n,R): m=k*n; props=range(1<