Q:
What are the arguments of the mathematicians who objected against the ontological argument/proof Gödel offered?
$$ \begin{array}{rl} \text{Ax. 1.} & \left\{P(\varphi) \wedge \Box \; \forall x[\varphi(x) \to \psi(x)]\right\} \to P(\psi) \\ \text{Ax. 2.} & P(\neg \varphi) \leftrightarrow \neg P(\varphi) \\ \text{Th. 1.} & P(\varphi) \to \Diamond \; \exists x[\varphi(x)] \\ \text{Df. 1.} & G(x) \iff \forall \varphi [P(\varphi) \to \varphi(x)] \\ \text{Ax. 3.} & P(G) \\ \text{Th. 2.} & \Diamond \; \exists x \; G(x) \\ \text{Df. 2.} & \varphi \text{ ess } x \iff \varphi(x) \wedge \forall \psi \left\{\psi(x) \to \Box \; \forall y[\varphi(y) \to \psi(y)]\right\} \\ \text{Ax. 4.} & P(\varphi) \to \Box \; P(\varphi) \\ \text{Th. 3.} & G(x) \to G \text{ ess } x \\ \text{Df. 3.} & E(x) \iff \forall \varphi[\varphi \text{ ess } x \to \Box \; \exists y \; \varphi(y)] \\ \text{Ax. 5.} & P(E) \\ \text{Th. 4.} & \Box \; \exists x \; G(x) \end{array} $$
I want to learn. Because, Gödel's proof was checked on the computer. Well, How can mathematicians criticize, if Gödel's proof is controlled by the computer and known to be true?I cannot understand how an object that is external is mathematically proven. What did the computer actually confirm?
I want to know the problems in Gödel's proof.
Any book or link you recommend , or answer will satisfy me.
The proof is of course, sound. But to claim that this argument proves that God as we understand exists, you also need to argue that the axioms really hold in the real world, which I believe would be extremely hard.
Edit : Another criticism comes from the fact that the same axioms can be used to prove that there must be infinitely many semi-gods.