Gödel's ontological proof and “modal collapses”

Recent findings on Gödel's ontological argument allowed to ultimately establish a couple of things:

• Gödel's original axiomata are inconsistent
• Scott's variation instead is consistent
• Scott's axioms imply the "modal collapse": every true statement is also necessarily true: $$\forall \phi(\phi \to \square \phi)$$

and it is said that this modal collapse is an unwanted/unacceptable consequence so that there have been proposal to slightly change the argument in order to avoid it.

I have some questions:

1. If in spite of the modal collapse the axioms are consistent why don't we just rephrase all the axioms without any modal operators at all and are happy with this new version of the argument? What would be so unsatisfying in a non-modal version of the argument? Maybe the axioms would become unreasonable/pointless?

2. Did anyone ever try to check if any of the proposed alternatives actually avoid the collapse?

Edit:

Here is how the argument would look like in the non-modal version: $$\begin{array}{rl} \text{Ax. 1.} & \left\{P(\varphi) \wedge \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 \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.} & \exists x \; G(x) \end{array}$$

The theorems can be derived following the same lines of the original proof with omitted modal operators for every statement. For example to prove Theorem 1: suppose we had $P(\varphi)$ and $\neg \exists x[\varphi(x)]$ then $\forall x[\varphi(x) \to \psi(x)]$ is vacously true for any $\psi$ and by Axiom 1 $P(\psi)$ is true for any possible $\psi$, that implies also $P(\neg \varphi)$ would be true violating Axiom 2. Then Theorem 2 follows by Axiom 3 and Theorem 1 even ignoring Definition 1.

What is so undesirable in this shorter argument compared to the modal-logic original one?

Gödel/Scott themselves use both Ax. 2 and Ax. 3. The only difference is in Axiom 1 where you omit the box operator inside the scope of the allquantifier.

Here is why I think this is a troublesome assumption. It might well be that it is accidentally the case that all individuals in our World that have a certain positive property A also have a Property B. For example: Suppose only humans have an appreciation for beauty, and that this is a positive property [our property A].

By Ax. 1 it would follow that every property B that all humans possess is also a positive property; Simply because

"$A(x) \rightarrow ishuman(x)$" and "$ishuman(x) \rightarrow B(x)$" implies "$A(x) \rightarrow B(x)$"

This is a conclusion that is - to say the least - not very intuitive. That would mean that every contingent feature of human biology [from blood circulation to being able to be killed by a stick] is a positive, even godly property. Gödels formulation avoid these pitfalls and seems to be more plausible.

Not an expert but familiar enough with this particular subject, i'd be more than happy if one could correct me on each point. First it was already established that Gödel's original proof suffered from modal collapse, as Sobel showed.

1. If you phrased everything without using modals then you wont be able to use some arguably crucial axioms and theorems in your proof such as S5, such as $$\lozenge\square\phi\equiv\square\phi$$
2. It seems Anderson published a revised version of his proof, didn't check his paper. However I know that Petr Hàjek published a paper titled A New Small Emendation of Gödel's Ontological Proof where affirms that Anderson's emendation "ha[s] no collapse" (p.1). He also proposed a further weakening of some of the axioms proposed by Anderson.
• I found this interesting summary about the achievements of the suggested variations by Anderson and Hàjek: github.com/FormalTheology/GoedelGod/blob/master/Papers/… – Marco Disce May 8 '16 at 15:32
• "If you phrased everything without using modals then you wont be able to use some arguably crucial axioms and theorems in your proof" but as far as I can see the non-modal version of these modal axioms are trivially true! – Marco Disce May 8 '16 at 15:42
• how would you go about phrasing $\diamond\square\phi\equiv\square\phi$ in your non-modal system? – user153330 May 8 '16 at 15:44
• Just $\phi \equiv \phi$ – Marco Disce May 8 '16 at 15:47
• but can you show how you prove theorem 1 and 2 in your non-modal system in your edit? – user153330 May 8 '16 at 22:47