Amidst the array of criticisms levied against Kurt Gödel’s ontological proof, the critique by Randolph Rubens Goldman stands out for its unique emphasis on a hitherto overlooked yet pivotal weakness within the proof – its lack of an adequate applied semantics. Goldman’s perspective underscores a significant need: the connection of axioms, definitions, and theorems in the proof with the intended meanings of properties traditionally ascribed to God. However, as Goldman has shown, this attempt poses formidable challenges. The endeavour to establish (...) such a connection renders numerous sentences under the natural language interpretation of the proof meaningless, thus undermining the principle of bivalence. In this article, we analyse different methods to confront this problem. Our final solution is inspired by Bertrand Russell’s theory of definite descriptions: namely, we suggest construing sentences under the natural language interpretation of Gödel’s proof as conjunctions of formulas. In this way, we can eliminate meaningless sentences and uphold the once unsettled principle of bivalence. (shrink)