Modal Logic: Possible Necessity implies Necessity in Godel's Ontological Proof?

Question

I am trying to understand Godel's Ontological proof, following these notes by Christopher Small. As I have no background in logic, I am picking up what's necessary from modal logic as I read.

I am in particular stuck at the very last few steps of the proof, where one goes from the statement

it is possibly necessary for a god-like individual to exist

to the statement

it is necessary for a god-like individual to exist

In the notes of Small, he says this follows from the "contrapositive of Becker's postulate":

Here, $G$ is the predicate of being god-like, defined as the conjunction of all positive attributes.

In addition, (M6) refers to the modal axiom $$\Diamond p\to \Box \Diamond p$$ However, I am unable to see how the contrapositive of this implies the desired result.

There is a very helpful answer by @mjqxxxx for this problem asked on Stackexchange, regarding how to understand Godel's proof. Unfortunately, this very last step, in this particular answer, does not have an explanation:

it's possible that it's necessary for something godlike to exist; and so it is, in fact, necessary for something godlike to exist

And thus ends the proof of the final Theorem.

I believe it is possible that my elementary understanding of basic Modal logic is not allowing me to see something that is perhaps very obvious. I would greatly appreciate any help on this. Thank you.

Answer 1

First of all, the contrapositive of $\varphi\to \psi$ is $\lnot \psi\to \lnot \varphi$.

So the contrapositive of $\lozenge p\to \square\lozenge p$ is $\lnot \square \lozenge p\to \lnot \lozenge p$.

Now in modal logic, negation switches boxes and diamonds: $\lnot \square \varphi$ is equivalent to $\lozenge \lnot \varphi$ and $\lnot \lozenge \varphi$ is equivalent to $\square \lnot \varphi$. I suspect this is the key thing you were missing.

So our contrapositive is equivalent to $\lozenge \square \lnot p\to \square \lnot p$.

Now substitute $\lnot (\exists y\, G(y))$ for $p$. The double negations cancel, and we get $\lozenge \square (\exists y\, G(y))\to \square (\exists y\, G(y))$.

By the way, I had never heard $\lozenge p\to \square\lozenge p$ referred to as "Becker's postulate" before. It is more common to refer to this axiom as "5" (see here or here, for example). Because of this numerical convention, it's rather unfortunate that the notes you're reading refer to it as (M6).