Types, Tableaus, and Gödel's God

Gödel's modal ontological argument is the centrepiece 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, semantically and through tableau rules, to produce a modified version of Montague/Gallin intensional logic. Extensionality, rigidity, equality, identity, and definite descriptions are investigated. Finally, vario...