Magari and others on Gödel’s ontological proof

Gödel’s proof of the necessary existence of God is analyzed from the point of view of modal logic together with related papers by Magari and Anderson. In particular, Magari’s claim on redundance in Gödel’s axioms is analyzed and shown to be only true for some extension of Gödel’s system (but true for Anderson’s modification, as it was shown elsewhere). Completeness of the underlying modal logic is proved; and it is shown that the “ontological” proof may use only the logic KD45 (logic of belief) instead of S5 (logic of knowledge).