Abstract

Sobel's modal collapse objection (1987, 2004) presupposes that Gödel's ontological proof is framed in S5 possible-worlds semantics Gödel never supplied. His 1952–54 version predates Kripke's framework by seven years; the later manuscripts record no conversion of the modal operators from iterative stability to truth-across-worlds, nor any shift from treating the divine monad as the limit of closure on positive properties. His consistent treatment of necessity as fixed-point stability under reflection extends naturally to the ontological proof. We present a machine-verified reconstruction in Isabelle/ZF, faithful to Gödel's Maximen notebooks and Wang's post-1970 reports, in which no axiom is added, weakened, or modified. Under this reading, axioms A2, A4, A5, and conjunction closure are derivable from the closure operator; A1 (polarity) alone is irreducible; and A3 (Godlike-positivity) holds as a consequence in compatible models. No modal collapse arises. Four decades of repair literature addressed a different proof.