[FOM] The characteristic S5 axiom and the ontological argument
alama at stanford.edu
Mon Apr 6 22:55:46 EDT 2009
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 Alama (alama at stanford.edu)
More information about the FOM