Gödel's modal ontological argument is the centerpiece of an extensive examination of intensional logic. First, classical type theory is presented semantically, tableau rules for it are introduced, and the Prawitz/Takahashi completeness proof is given. Then modal machinery is added to produce a modified version of Montague/Gallin intensional logic. Finally, various ontological proofs for the existence of God are discussed informally, and the Gödel argument is fully formalized. Parts of the book are mathematical, parts philosophical.

Kurt Gödel’s version of the ontological argument was shown by J. Howard Sobel to be defective, but some plausible modifications in the argument result in a version which is immune to Sobel’s objection. A definition is suggested which permits the proof of some of Godel’s axioms.

The aim of this paper is to prove strong completeness theorems for several Anderson-like variants of Gödels theory wrt. classes of modal structures, in which: (i). 1st order terms order receive only rigid extensions in the constant objectual 1st order domain; (ii). 2nd order terms receive non-rigid extensions in preselected world-relative objectual domains of 2nd order and rigid intensions in the constant conceptual 2nd order domain.