Axioms in Gödel's ontological proof are inconsistent?

Question

So, my problem is with Axiom 5 of the proof, where Gödel considers necessary existence as a property. However, by his own definition, a 'property' applies to objects including those whose necessary existence has not even been proven, as can be inferred from Theorem 1. This, to me, seems like the perfect example of question begging, and if such logic is to be used on other examples, the conclusions may be contradictory. For example, I can prove that a Godlike object doesn't exist using the same logic and assuming Gödel's axioms:

1. $Df. 1:A_φ(x)⇔(◇∃x⇒(◻∃x∧φ(x)))$
2. $Ax. 1:(P(φ)∧◻∀x(φ(x)⇒ψ(x)))⇒P(ψ)$
3. $Ax. 2:P(¬φ)⇔¬P(φ)$
4. $Th. 1:P(φ)⇒◇∃x(φ(x))$
5. $Ax. 3:P(◇∃x⇒◻∃x)$
6. $Th. 2:∀φ(P(φ)⇒◻∃x(A_φ(x))$

Ax.3 is inferred from Gödel's fifth axiom, where necessary existence is a positive property. From here, I can conclude that any positive property that one can think of exists. For example, if being a unicorn is a positive property (which it is) then invisible flying unicorns also exist (because God is also flying and invisible, so these are positive properties).

Note that I didn't, in any way, deviate from the axioms in Gödel's original theorem, and I didn't add any extra ones.

Obviously, though, it is very unlikely that I've just proven Gödel's proof to be wrong, so my 'theorem' must be wrong. However, I've followed through each of the steps in my 'proof' many times over and didn't manage to find any deviation from Gödel's axioms either time. Can anyone help me with this?

Answer 1

Note that Theorem 1 of your link actually states: $P(\phi) \implies \Diamond \exists x \phi(x)$, i.e. if $\phi$ is a positive property, then possibly there is something that instantiates it. Given this, Gödel needs an explicit axiom stating that being god-like is a positive property (Axiom 3 in your link: $P(G)$). So, in order for your proof to go through by use of Theorem 1, you'll need an analogous Axiom 3$'$, stating that $A(x)$ is a positive property. But then: (i) you'll have introduced an extra axiom, extraneous to Gödel's own axioms, and (ii) this axiom is not very plausible. So there is no contradiction among Gödel's own axioms.

Answer 2

I havent read too far into it, but i think these authors embedded the higher order modal argument into higher order logic, and proved their embedding is consistent: https://www.google.com/url?sa=t&source=web&rct=j&url=http://page.mi.fu-berlin.de/cbenzmueller/papers/C40.pdf&ved=0ahUKEwiciojM14_XAhVDRCYKHVc1CpwQFghYMAQ&usg=AOvVaw0iNVCeRqSVtD-hbE4IoPjn

However, the same authors were able to put the original argument into an extremely novel higher order modal logic prover, and they found an inconsistency that had never before appeared in the literature: https://www.google.com/url?sa=t&source=web&rct=j&url=https://www.ijcai.org/Proceedings/16/Papers/137.pdf&ved=0ahUKEwiIu4yg2o_XAhUGJiYKHSTZANAQFghsMAY&usg=AOvVaw3A4fyJ-0UUFYRmeWfjgUAX

I dont fully understand your objection, and I think they agree that axiom 5 is one of the faulty steps, but anyways these papers seem like a good place to start. Pretty deep stuff!