[FOM] The characteristic S5 axiom and the ontological argument

[Alex Blum]

I wonder if Godel noticed that the characteristic S5 axiom:

'If Pos Nec p then Nec p',

will give him straightaway the skeleton of the ontological proof for the 
existence of God; and that what remains is the not easy task to prove 
the consistency of 'God exists'.
For what the skeleton of the argument proves is that: if it is possible 
that God exists necessarily then God exists necessarily, which is but an 
instance of the characteristic S5 axiom.
It could very well be that his suspicion of the characteristic S5 axiom 
held him back.
Alex Blum