[FOM] The characteristic S5 axiom and the ontological argument

[Jesse Alama]

Alex Blum <blumal-WCJ8v+0vi+56auLlOhE+pQ at public.gmane.org> writes:

> 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.

The S5 axiom is indeed used in a crucial way, though, as you point out,
a lot more work is required than just appealing to that axiom.  See
Melvin Fitting's _Types, Tableaus, and Gödel's God_ for a detailed
presentation of Gödel's ontological argument.  (Fitting uses a
higher-order formalism, not just propositional S5.)

Jesse

-- 
Jesse Alama (alama at stanford.edu)